Commit 2024-11-18 02:41 25f427c3

View on Github →

feat(SetTheory/Cardinal/Aleph): some lemmas on omega (#18542)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.isLimit_omega

added theorem Ordinal.lift_omega

added theorem Ordinal.lift_preOmega

added theorem Ordinal.omega_pos

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.omega_pos

Modified Mathlib/SetTheory/Ordinal/Basic.lean