Theorem Order.isSuccPrelimit_iff_forall_lt_nonempty_Ioo

Modification history

2026-09-13 22:38
Mathlib/Order/SuccPred/Limit.lean
feat(Order/SuccPred/Limit): small theorems and generalizations (#42480) …
Added Order.isSuccPrelimit_iff_forall_lt_nonempty_IooView on Github →