Commit 2026-04-02 14:00 b31b6018

View on Github →

chore: rename isSuccLimit_iff → isSuccLimit_iff_of_orderBot (#37410) I've been bitten a few times by trying to apply this lemma in orders where it's not applicable.

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.isSuccLimit_iff

added theorem Order.isSuccLimit_iff_of_orderBot

Modified Mathlib/SetTheory/Cardinal/Order.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.isSuccLimit_iff