lt_iff_sub_pos — Mathlib

English

x < y if and only if 0 < y − x.

Русский

x < y тогда и только тогда, когда 0 < y − x.

LaTeX

$$$ x < y \\iff 0 < y - x $$$

Lean4

theorem lt_iff_sub_pos {x y : PGame} : x < y ↔ 0 < y - x :=
  ⟨fun h => lt_of_le_of_lt (zero_le_add_neg_cancel x) (add_lt_add_right h _), fun h =>
    calc
      x ≤ 0 + x := (PGame.zero_add x).symm.le
      _ < y - x + x := (add_lt_add_right h _)
      _ ≤ y + (-x + x) := (PGame.add_assoc _ _ _).le
      _ ≤ y + 0 := by gcongr; exact neg_add_cancel_le_zero x
      _ ≤ y := (PGame.add_zero y).le⟩

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