Commit 2026-03-27 12:01 816ff458

View on Github →

feat(SetTheory/Ordinal): small lemmas on ⨆ i, f i + 1 (#37264) In preparation for deprecating Ordinal.lsub.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

added theorem Ordinal.iSup_add_one_le

added theorem Ordinal.iSup_add_one_le_iff

modified theorem Ordinal.lsub_le_iff

added theorem Ordinal.lt_iSup_add_one

added theorem Ordinal.lt_iSup_add_one_iff