omega — Mathlib

English

preOmega is a normal function.

Русский

preOmega — обычная функция.

LaTeX

$$$\mathrm{IsNormal}(\mathrm{preOmega})$$$

Lean4

/-- The `omega` function gives the infinite initial ordinals listed by their ordinal index.
`omega 0 = ω`, `omega 1 = ω₁` is the first uncountable ordinal, and so on.

This is not to be confused with the first infinite ordinal `Ordinal.omega0`.

For a version including finite ordinals, see `Ordinal.preOmega`. -/
def omega : Ordinal ↪o Ordinal :=
  (OrderEmbedding.addLeft ω).trans preOmega

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