Theorem Order.not_isSuccPrelimit_iff_succ_eq

Modification history

2026-05-01 13:07
Mathlib/Order/SuccPred/Limit.lean
chore: `not_isSuccLimit_iff` → `not_isSuccLimit_iff_succ_eq` (#38235) …
Added Order.not_isSuccPrelimit_iff_succ_eqView on Github →