English
If a PGame is short, its birthday is a finite ordinal, i.e., less than ω0.
Русский
Если PGame короткая, то её день рождения является конечной ординалой, то есть меньше ω0.
LaTeX
$$$ Short(x) \Rightarrow x.birthday < \omega_0 $$$
Lean4
theorem short_birthday (x : PGame.{u}) : [Short x] → x.birthday < Ordinal.omega0 := by
-- Porting note: Again `induction` is used instead of `pgame_wf_tac`
induction x with
| mk xl xr xL xR ihl ihr =>
intro hs
rcases hs with ⟨sL, sR⟩
rw [birthday, max_lt_iff]
constructor
all_goals
rw [← Cardinal.ord_aleph0]
refine
Cardinal.lsub_lt_ord_of_isRegular.{u, u} Cardinal.isRegular_aleph0 (Cardinal.lt_aleph0_of_finite _) fun i => ?_
rw [Cardinal.ord_aleph0]
· apply ihl
· apply ihr
