Commit 2026-05-01 13:07 0797a974

View on Github →

chore: not_isSuccLimit_iff → not_isSuccLimit_iff_succ_eq (#38235) A lemma with such a simple name as not_isSuccLimit_iff shouldn't require a partial successor order! The new not_isSuccLimit_iff is a straightforward unfolding of the definitions and requires only a preorder.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/SuccPred/Limit.lean

modified theorem Order.isSuccPrelimit_of_succ_lt

deleted theorem Order.not_isSuccPrelimit_iff'

modified theorem Order.not_isSuccPrelimit_iff

deleted theorem Order.not_isSuccPrelimit_iff_exists_covBy

added theorem Order.not_isSuccPrelimit_iff_mem_range_succ

added theorem Order.not_isSuccPrelimit_iff_succ_eq

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/Topology/Order/SuccPred.lean