Commit 2025-04-15 10:53 a9eda3d7

View on Github →

feat: add characterisation of closed interval for locally-finite conditionally complete linear orders (#23910)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Interval/Set/OrdConnectedLinear.lean

added theorem Set.Nonempty.eq_Icc_iff_int

added theorem Set.Nonempty.eq_Icc_iff_nat

added theorem Set.Nonempty.ordConnected_iff_of_bdd'

added theorem Set.Nonempty.ordConnected_iff_of_bdd

added theorem Set.ordConnected_iff_disjoint_Ioo_empty

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem Order.Ioo_eq_empty_iff_le_succ

added theorem Order.Ioo_eq_empty_iff_pred_le