Theorem Order.Ioo_eq_empty_iff_le_succ

Modification history

2025-04-15 10:53
Mathlib/Order/SuccPred/Basic.lean
feat: add characterisation of closed interval for locally-finite conditionally complete linear orders (#23910)
Added Order.Ioo_eq_empty_iff_le_succView on Github →