Theorems · Definition · logic and foundations

Ordinal.preOmega

Ordinal.{u} ↪o Ordinal.{u}

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.

Defined in

Mathlib.SetTheory.Cardinal.Aleph

Cited by

31 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound