Theorem Order.isSuccPrelimit_of_succ_lt

Modification history

2026-05-01 13:07
Mathlib/Order/SuccPred/Limit.lean
chore: `not_isSuccLimit_iff` → `not_isSuccLimit_iff_succ_eq` (#38235) …
Modified Order.isSuccPrelimit_of_succ_ltView on Github →
2024-09-06 21:42
Mathlib/Order/SuccPred/Limit.lean
refactor(Order/SuccPred/Limit): `IsSuccLimit` → `IsSuccPrelimit` (#16518) …
Added Order.isSuccPrelimit_of_succ_ltView on Github →