English
For pre-games x and y, x is related to y by the left-right relation if and only if either there exists a Left move i with x ≤ y.moveLeft i, or there exists a Right move j with x.moveRight j ≤ y.
Русский
Для пред-игр x и y выполнение отношения LF эквивалентно тому, что или существует ход слева i, такой что x ≤ y.moveLeft i, или существует ход справа j, такой что x.moveRight j ≤ y.
LaTeX
$$$x \\\\mathrm{⧏}\\\\ y \\\\iff \\\\Big(\\\\exists i, x \\\\le y.moveLeft i\\\\Big) \\\\lor \\\\Big(\\\\exists j, x.moveRight j \\\\le y\\\\Big)$$$
Lean4
/-- Definition of `x ⧏ y` on pre-games, in terms of `≤`.
The ordering here is chosen so that `or.inl` refer to moves by Left, and `or.inr` refer to
moves by Right. -/
theorem lf_iff_exists_le {x y : PGame} : x ⧏ y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y :=
by
rw [LF, le_iff_forall_lf, not_and_or]
simp
