toPGameEmbedding — Mathlib

English

There is an order-embedding from Ordinal into PGame given by a ↦ toPGame(a).

Русский

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

LaTeX

$$$\mathrm{toPGameEmbedding} : \mathrm{Ordinal} \hookrightarrow^{\mathrm{ord}} \mathrm{PGame}$$$

Lean4

/-- The order embedding version of `toPGame`. -/
@[simps]
noncomputable def toPGameEmbedding : Ordinal.{u} ↪o PGame.{u}
    where
  toFun := Ordinal.toPGame
  inj' := toPGame_injective
  map_rel_iff' := @toPGame_le_iff

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