Commit 2026-03-25 04:37 56a14629

View on Github →

feat(SetTheory/Ordinal): fundamental sequences (#37019) We redefine a fundamental sequence for an ordinal o as a strict monotonic function Iio o.cof.ord → Iio o with cofinal range. We reprove the API on the pre-existing predicate, and deprecate it.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Cofinal.lean

added theorem OrderIso.map_isCofinal_iff

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

deleted theorem Ordinal.IsFundamentalSequence.blsub_eq

deleted theorem Ordinal.IsFundamentalSequence.id_of_le_cof

deleted theorem Ordinal.IsFundamentalSequence.of_isNormal

deleted theorem Ordinal.IsFundamentalSequence.ord_cof

deleted theorem Ordinal.IsFundamentalSequence.trans

deleted def Ordinal.IsFundamentalSequence

deleted theorem Ordinal.exists_fundamental_sequence

Created Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

added theorem Ordinal.IsFundamentalSeq.comp_isNormal

added theorem Ordinal.IsFundamentalSeq.iSup_add_one_eq

added theorem Ordinal.IsFundamentalSeq.iSup_eq

added theorem Ordinal.IsFundamentalSeq.ord_cof

added structure Ordinal.IsFundamentalSeq

added theorem Ordinal.IsFundamentalSequence.blsub_eq

added theorem Ordinal.IsFundamentalSequence.id_of_le_cof

added theorem Ordinal.IsFundamentalSequence.of_isNormal

added theorem Ordinal.IsFundamentalSequence.ord_cof

added theorem Ordinal.IsFundamentalSequence.trans

added def Ordinal.IsFundamentalSequence

added theorem Ordinal.exists_fundamental_sequence

added theorem Ordinal.exists_isFundamentalSeq