English
Characterization of ≤ via moves: x ≤ y iff certain left-move and right-move conditions hold.
Русский
Характеризация отношения ≤ через ходы слева и справа.
LaTeX
$$$$ x \\\\le y \\\\iff \\\\text{(left-move condition)} \\\\land \\\\text{(right-move condition)}. $$$$
Lean4
/-- The definition of `x ≤ y` on pre-games, in terms of `≤` two moves later.
Note that it's often more convenient to use `le_iff_forall_lf`, which only unfolds the definition by
one step. -/
theorem le_def {x y : PGame} :
x ≤ y ↔
(∀ i, (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧
∀ j, (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j :=
by
rw [le_iff_forall_lf]
conv =>
lhs
simp only [lf_iff_exists_le]
