Commit 2024-10-23 21:11 ca0f1392

View on Github →

feat(SetTheory/Cardinal/Aleph): introduce omega function (#17669) We introduce the preOmega function enumerating the initial ordinals, as well as the more standard omega skipping over finite ordinals.

Estimated changes

added theorem Ordinal.coe_preOmega
added theorem Ordinal.isNormal_omega
added theorem Ordinal.le_omega_self
added def Ordinal.omega
added theorem Ordinal.omega_le_omega
deleted theorem Ordinal.omega_lt_omega1
added theorem Ordinal.omega_lt_omega
added theorem Ordinal.omega_max
added theorem Ordinal.omega_zero
added def Ordinal.preOmega
added theorem Ordinal.preOmega_max
added theorem Ordinal.preOmega_ofNat
added theorem Ordinal.preOmega_zero
added theorem Ordinal.range_omega
added theorem Ordinal.range_preOmega