English
The preOmega function enumerates the initial ordinals by their ordinal index.
Русский
Функция preOmega перечисляет начальные ординалы по их индексам-ордналам.
LaTeX
$$$\mathrm{preOmega} : \mathrm{Ordinal} \hookrightarrow_o \mathrm{Ordinal}$ with toFun(o) = \mathrm{enumOrd}\{x \mid \mathrm{IsInitial}(x)\}$$$
Lean4
/-- The "pre-omega" function gives the initial ordinals listed by their ordinal index.
`preOmega n = n`, `preOmega ω = ω`, `preOmega (ω + 1) = ω₁`, etc.
For the more common omega function skipping over finite ordinals, see `Ordinal.omega`. -/
def preOmega : Ordinal.{u} ↪o Ordinal.{u}
where
toFun := enumOrd {x | IsInitial x}
inj' _ _ h := enumOrd_injective not_bddAbove_isInitial h
map_rel_iff' := enumOrd_le_enumOrd not_bddAbove_isInitial
