Theorem Order.Ioo_eq_empty_iff_pred_le

Modification history

2026-05-01 14:40
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Basic): use `to_dual` more (#38653)
Deleted Order.Ioo_eq_empty_iff_pred_leView on Github →
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 →