birthday_star — Mathlib

English

The birthday of the star game is 1.

Русский

День рождения звезды равен 1.

LaTeX

$$$\operatorname{birthday}(\text{star}) = 1$$$

Lean4

@[simp]
theorem birthday_star : birthday ⟦PGame.star⟧ = 1 :=
  by
  apply le_antisymm
  · rw [← PGame.birthday_star]
    exact birthday_quot_le_pGameBirthday _
  · rw [Ordinal.one_le_iff_ne_zero, ne_eq, birthday_eq_zero, Game.zero_def, ← PGame.equiv_iff_game_eq]
    exact PGame.star_fuzzy_zero.not_equiv

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