Commit 2026-10-17 11:31 abb44da2

View on Github →

feat: every element is between two others in a club set (#44793) As well as further lemmas about normal functions and club sets. Used in the CGT repo.

Estimated changes

Modified Mathlib/Order/Cofinal.lean

added theorem IsCofinal.noMaxOrder

Modified Mathlib/Order/IsNormal.lean

modified theorem Order.IsNormal.dirSupClosed_range

added theorem Order.IsNormal.dirSupClosed_range_of_isCofinal

added theorem Order.IsNormal.of_dirSupClosed_range

added theorem Order.isNormal_iff_dirSupClosed_range

added theorem Order.isNormal_iff_dirSupClosed_range_of_isCofinal

Modified Mathlib/Order/WellFounded.lean

added theorem StrictMono.isCofinal_range_of_wellFoundedLT

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

added theorem IsClub.exists_between

added theorem IsClub.isNormal_subtypeVal

added theorem Order.isNormal_iff_isClub_range

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

modified theorem Order.isNormal_enum_iff_dirSupClosed