Commit 2026-04-19 12:49 700fcd70

View on Github →

refactor: isSuccPrelimit_iff → isSuccPrelimit_iff_isMin (#38238) We rename some lemmas on succ-archimedean orders with names suggesting much more general theorems.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.isSuccPrelimit_iff

added theorem Order.isSuccPrelimit_iff_isMin

deleted theorem Order.not_isSuccLimit

added theorem Order.not_isSuccLimit_of_isSuccArchimedean

deleted theorem Order.not_isSuccPrelimit

added theorem Order.not_isSuccPrelimit_of_isSuccArchimedean