English
There exists an order-preserving embedding of the class of ordinals into the Surreal numbers, sending each ordinal to the surreal number obtained from its associated numeric game. In particular, there is an injective order-embedding φ: Ord → Surreal with φ(o) equal to the surreal number corresponding to the numeric game of o for every ordinal o.
Русский
Существует вложение порядка от множества ординалов в множество сюрреалов, которое отображает каждый ординал в соответствующее сюрреальное число, получаемое из числовой игры, ассоциированной с этим ординалом. То есть существует инъективное вложение φ: Ord → Surreal такое, что для каждого ординала o выполняется φ(o) — сюрреальное число, соответствующее числовой игре o.
LaTeX
$$$\exists \varphi: \mathrm{Ord} \hookrightarrow \mathrm{Surreal}, \forall o \in \mathrm{Ord}, \ \varphi(o) = \llbracket \operatorname{numeric\_toPGame}(o) \rrbracket.$$$
Lean4
/-- Converts an ordinal into the corresponding surreal. -/
noncomputable def toSurreal : Ordinal ↪o Surreal
where
toFun o := mk _ (numeric_toPGame o)
inj' a b
h :=
toPGame_equiv_iff.1
(by apply Quotient.exact h) -- Porting note: Added `by apply`
map_rel_iff' := @toPGame_le_iff
