Documentation

Mathlib.Order.Interval.Set.OrdConnectedLinear

Order-connected subsets of linear orders #

In this file we provide some results about order-connected subsets of linear orders, together with some convenience lemmas for characterising closed intervals in certain concrete types such as , , and Fin n.

Main results: #

A version of Set.Nonempty.ordConnected_iff_of_bdd for complete linear orders, such as Fin n, in which the explicit boundedness hypotheses are not necessary.

theorem Set.ordConnected_iff_disjoint_Ioo_empty {α : Type u_1} {I : Set α} [LinearOrder α] [LocallyFiniteOrder α] :
I.OrdConnected xI, yI, Disjoint (Ioo x y) IIoo x y =
theorem Set.Nonempty.eq_Icc_iff_nat {I : Set } (h₀ : I.Nonempty) (h₂ : BddAbove I) :
I = Icc (sInf I) (sSup I) xI, yI, Disjoint (Ioo x y) Iy x + 1
theorem Set.Nonempty.eq_Icc_iff_int {I : Set } (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I) :
I = Icc (sInf I) (sSup I) xI, yI, Disjoint (Ioo x y) Iy x + 1