English
For any ordinal o, the birthday of Nim(o) is o; i.e., nim o has birthday o.
Русский
Для любого порядка o день рождения Nim(o) равен o; то есть Nim(o) имеет день рождения o.
LaTeX
$$$ \operatorname{birthday}(\mathrm{nim}(o)) = o. $$$
Lean4
@[simp]
theorem nim_birthday (o : Ordinal) : (nim o).birthday = o :=
by
induction o using Ordinal.induction with
| _ o IH
rw [nim, birthday_def]
dsimp
rw [max_eq_right le_rfl]
convert lsub_typein o with i
exact IH _ (typein_lt_self i)