English
For numeric x,y, either x < y, or x ≈ y, or y < x.
Русский
Для числовых x,y либо x < y, либо x ≈ y, либо y < x.
LaTeX
$$x < y ∨ (x ≈ y) ∨ y < x$$
Lean4
/-- The definition of `x < y` on numeric pre-games, in terms of `<` two moves later. -/
theorem lt_def {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
x < y ↔
(∃ i, (∀ i', x.moveLeft i' < y.moveLeft i) ∧ ∀ j, x < (y.moveLeft i).moveRight j) ∨
∃ j, (∀ i, (x.moveRight j).moveLeft i < y) ∧ ∀ j', x.moveRight j < y.moveRight j' :=
by
rw [← lf_iff_lt ox oy, lf_def]
refine or_congr ?_ ?_ <;> refine exists_congr fun x_1 => ?_ <;> refine and_congr ?_ ?_ <;>
refine forall_congr' fun i => lf_iff_lt ?_ ?_ <;>
apply_rules [Numeric.moveLeft, Numeric.moveRight]
