le_iff_sub_nonneg — Mathlib

English

For any pgame x and y, x ≤ y if and only if y minus x is nonnegative.

Русский

Для любых игр x и y верно: x ≤ y тогда и только тогда, когда y − x неотрицательно.

LaTeX

$$$ x \\le y \\iff 0 \\le y - x $$$

Lean4

theorem le_iff_sub_nonneg {x y : PGame} : x ≤ y ↔ 0 ≤ y - x :=
  ⟨fun h => (zero_le_add_neg_cancel x).trans (add_le_add_right h _), fun h =>
    calc
      x ≤ 0 + x := (PGame.zero_add x).symm.le
      _ ≤ y - x + x := by gcongr
      _ ≤ y + (-x + x) := (PGame.add_assoc _ _ _).le
      _ ≤ y + 0 := (add_le_add_left (neg_add_cancel_le_zero x) _)
      _ ≤ y := (PGame.add_zero y).le⟩

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