nim_birthday — Mathlib

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)

Похожие утверждения