Theorem Order.IsSuccPrelimit.lt_iff_exists_lt

Modification history

2026-09-13 22:38
Mathlib/Order/SuccPred/Limit.lean
feat(Order/SuccPred/Limit): small theorems and generalizations (#42480) …
Deleted Order.IsSuccPrelimit.lt_iff_exists_ltView on Github →
2024-09-23 19:41
Mathlib/Order/SuccPred/Limit.lean
feat(Order/SuccPred/Limit): `IsSuccPrelimit.le_iff_forall_le` (#17026)
Added Order.IsSuccPrelimit.lt_iff_exists_ltView on Github →