lt_iff_exists_le — Mathlib

English

If there exists i with x ≤ y.moveLeft i or exists j with x.moveRight j ≤ y, then x < y.

Русский

Существуют i или j такие, что x < y(после преобразования), если существуют соответствующие неравенства.

LaTeX

$$$((\exists i, x \le y.moveLeft i) \lor\ (\exists j, x.moveRight j \le y)) \Rightarrow x < y$$$

Lean4

/-- Definition of `x < y` on numeric pre-games, in terms of `≤` -/
theorem lt_iff_exists_le {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y := by rw [← lf_iff_lt ox oy, lf_iff_exists_le]

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