English
Characterization of when a number o is less than x's birthday in terms of left and right moves.
Русский
Характеризация того, когда число o меньше birthday x через левые и правые ходы.
LaTeX
$$$ o < x.birthday \iff (\exists i \in x.LeftMoves, o \le (x.moveLeft i).birthday) \lor (\exists i \in x.RightMoves, o \le (x.moveRight i).birthday) $$$
Lean4
theorem lt_birthday_iff {x : PGame} {o : Ordinal} :
o < x.birthday ↔
(∃ i : x.LeftMoves, o ≤ (x.moveLeft i).birthday) ∨ ∃ i : x.RightMoves, o ≤ (x.moveRight i).birthday :=
by
constructor
· rw [birthday_def]
intro h
rcases lt_max_iff.1 h with h' | h'
· left
rwa [lt_lsub_iff] at h'
· right
rwa [lt_lsub_iff] at h'
· rintro (⟨i, hi⟩ | ⟨i, hi⟩)
· exact hi.trans_lt (birthday_moveLeft_lt i)
· exact hi.trans_lt (birthday_moveRight_lt i)
