English
Characterization of LF via a two-move unfolding: x ⧏ y is equivalent to a left-move witness or a right-move witness with LF relations.
Русский
Характеризация LF через развертывание на два хода: x ⧏ y эквивалентно существованию левого свидетеля или правого свидетеля с LF-отношениями.
LaTeX
$$$$ x \\mathbf{⧏} y \\iff \\Big( \\exists i, (\\\\forall i', x.moveLeft i' \\\\mathbf{⧏} y.moveLeft i) \\\\land \\\\forall j, x \\\\mathbf{⧏} (y.moveLeft i).moveRight j \\Big) \\\\lor \\\\Big( \\exists j, (\\\\forall i, (x.moveRight j).moveLeft i \\\\mathbf{⧏} y) \\\\land \\\\forall j', x.moveRight j \\\\mathbf{⧏} y.moveRight j' \\Big). $$$$
Lean4
/-- The definition of `x ⧏ y` on pre-games, in terms of `⧏` two moves later.
Note that it's often more convenient to use `lf_iff_exists_le`, which only unfolds the definition by
one step. -/
theorem lf_def {x y : PGame} :
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_exists_le]
conv =>
lhs
simp only [le_iff_forall_lf]
