birthday_ordinalToGame — Mathlib

English

For every ordinal o, the birthday of its associated game equals o.

Русский

Для любого ординала o день рождения соответствующей ему игры равен o.

LaTeX

$$$\operatorname{birthday}(\operatorname{toGame}(o)) = o$$$

Lean4

@[simp]
theorem birthday_ordinalToGame (o : Ordinal) : birthday o.toGame = o :=
  by
  apply le_antisymm
  · conv_rhs => rw [← PGame.birthday_ordinalToPGame o]
    apply birthday_quot_le_pGameBirthday
  · let ⟨x, hx₁, hx₂⟩ := birthday_eq_pGameBirthday o.toGame
    rw [← hx₂, ← toPGame_le_iff]
    rw [← mk_toPGame, ← PGame.equiv_iff_game_eq] at hx₁
    exact hx₁.2.trans (PGame.le_birthday x)

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