Theorem Order.Ioo_eq_empty_iff_pred_le

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_pred_leView on Github →