numeric_toPGame — Mathlib

English

Ordinal numbers are numeric when viewed as pre-games.

Русский

Порядковые числа числовы, когда рассматриваются как пред-игры.

LaTeX

$$forall o : Ordinal, (o.toPGame).Numeric$$

Lean4

/-- Ordinal games are numeric. -/
theorem numeric_toPGame (o : Ordinal) : o.toPGame.Numeric :=
  by
  induction o using Ordinal.induction with
  | _ o IH
  apply numeric_of_isEmpty_rightMoves
  simpa using fun i => IH _ (Ordinal.toLeftMovesToPGame_symm_lt i)

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