birthday_ordinalToPGame — Mathlib

English

For every ordinal o, o.toPGame.birthday = o.

Русский

Для каждого ординала o, birthday у o.toPGame равен o.

LaTeX

$$$ \forall o,\; o.toPGame.birthday = o $$$

Lean4

@[simp]
theorem birthday_ordinalToPGame (o : Ordinal) : o.toPGame.birthday = o :=
  by
  induction o using Ordinal.induction with
  | _ o IH
  rw [toPGame, PGame.birthday]
  simp only [lsub_empty, max_zero_right]
  conv_rhs => rw [← lsub_typein o]
  congr with x
  exact IH _ (typein_lt_self x)

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