add_lf_add_right — Mathlib

English

If y ⧏ z, then y + x ⧏ z + x for all x.

Русский

Если y ⧏ z, то y + x ⧏ z + x для любого x.

LaTeX

$$y + x \;⧏\; z + x$$

Lean4

theorem add_lf_add_right {y z : PGame} (h : y ⧏ z) (x) : y + x ⧏ z + x :=
  suffices z + x ≤ y + x → z ≤ y by
    rw [← PGame.not_le] at h ⊢
    exact mt this h
  fun w =>
  calc
    z ≤ z + 0 := (PGame.add_zero _).symm.le
    _ ≤ z + (x + -x) := (add_le_add_left (zero_le_add_neg_cancel x) _)
    _ ≤ z + x + -x := (PGame.add_assoc _ _ _).symm.le
    _ ≤ y + x + -x := by gcongr
    _ ≤ y + (x + -x) := (PGame.add_assoc _ _ _).le
    _ ≤ y + 0 := (add_le_add_left (add_neg_cancel_le_zero x) _)
    _ ≤ y := (PGame.add_zero _).le

Похожие утверждения