lt_of_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 с x ≤ y.moveLeft i или существует j с x.moveRight j ≤ y, то x < y.

LaTeX

$$(\exists i, x \le y.moveLeft i) ∨ (\exists j, x.moveRight j ≤ y) → x < y$$

Lean4

theorem lt_of_exists_le {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    ((∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) → x < y :=
  (lt_iff_exists_le ox oy).2

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