Commit 2026-07-03 00:00 6b955101

View on Github →

feat: more results on Order.enum (#39136) Most importantly, we prove that the enumerator function of a cofinal set is normal iff the set is closed (under non-empty suprema).

Estimated changes

Modified Mathlib/Order/Cofinal.lean

modified theorem IsCofinal.nonempty

added theorem isCofinal_range_of_strictMono

Modified Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

added theorem IsClub.isNormal_enum

added theorem Order.isNormal_enum_iff_isClub

Modified Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean

added theorem Order.enum_anti

added theorem Order.enum_bot

added theorem Order.enum_eq_iff

modified theorem Order.enum_le_of_forall_lt

added theorem Order.enum_range

modified theorem Order.enum_succ_le_of_lt

added theorem Order.isNormal_enum_iff_dirSupClosed

Modified Mathlib/SetTheory/Ordinal/Topology.lean