Commit 2026-06-02 11:56 b2113152

View on Github →

chore: make IsSuccLimit a structure (#38234) This lets us name the fields. Note that the mk_iff lemma overwrites a recently deprecated theorem.

Estimated changes

Modified Mathlib/Order/SuccPred/InitialSeg.lean

Modified Mathlib/Order/SuccPred/Limit.lean

added structure Order.IsPredLimit

added structure Order.IsSuccLimit

deleted def Order.IsSuccLimit

deleted theorem Order.IsSuccPrelimit.isSuccLimit