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:

• Set.ordConnected_iff_disjoint_Ioo_empty: a characterisation of Set.OrdConnected for locally-finite linear orders.
• Set.Nonempty.ordConnected_iff_of_bdd: a characterisation of closed intervals for locally-finite conditionally complete linear orders.
• Set.Nonempty.ordConnected_iff_of_bdd': a characterisation of closed intervals for locally-finite complete linear orders (convenient for Fin n).
• Set.Nonempty.eq_Icc_iff_nat: characterisation of closed intervals for ℕ.
• Set.Nonempty.eq_Icc_iff_int: characterisation of closed intervals for ℤ.

theorem Set.Nonempty.ordConnected_iff_of_bdd {α : Type u_1} {I : Set α} [ConditionallyCompleteLinearOrder α] [LocallyFiniteOrder α] (h₀ : I.Nonempty) (h₁ : BddBelow I) (h₂ : BddAbove I) : I.OrdConnected ↔ I = Icc (sInf I) (sSup I)

theorem Set.Nonempty.ordConnected_iff_of_bdd' {α : Type u_1} {I : Set α} [ConditionallyCompleteLinearOrder α] [OrderTop α] [OrderBot α] [LocallyFiniteOrder α] (h₀ : I.Nonempty) : I.OrdConnected ↔ I = Icc (sInf I) (sSup I)

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 ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → Ioo x y = ∅

theorem Set.Nonempty.eq_Icc_iff_nat {I : Set ℕ} (h₀ : I.Nonempty) (h₂ : BddAbove I) : I = Icc (sInf I) (sSup I) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ 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) ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Ioo x y) I → y ≤ x + 1