toGame — Mathlib

English

There is an order-embedding from Ordinal into Game, given by a ↦ ⟦a.toPGame⟧.

Русский

Существует отображение с сохранением порядка из Ordinal в Game, заданное a ↦ ⟦a.toPGame⟧.

LaTeX

$$$\mathrm{toGame} : \mathrm{Ordinal} \hookrightarrow^{\mathrm{ord}} \mathrm{Game}$$$

Lean4

/-- Converts an ordinal into the corresponding game. -/
noncomputable def toGame : Ordinal.{u} ↪o Game.{u}
    where
  toFun o := ⟦o.toPGame⟧
  inj' a b := by simpa [AntisymmRel] using le_antisymm
  map_rel_iff' := toPGame_le_iff

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