Commit 2026-10-10 11:48 ec401114

View on Github →

chore: redefine Ordinal.preOmega using Order.enum (#39847) The plan is to deprecate Ordinal.enumOrd in favor of Order.enum.

Estimated changes

Modified Counterexamples/Omega1Space.lean

Modified Mathlib/Order/Cofinal.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Ordinal.coe_preOmega

added theorem Ordinal.isCofinal_setOfPred_isInitial

modified theorem Ordinal.not_bddAbove_isInitial

modified theorem Ordinal.preOmega_zero

modified theorem Ordinal.range_preOmega