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 ofSet.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 forFin 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)
:
theorem
Set.Nonempty.ordConnected_iff_of_bdd'
{α : Type u_1}
{I : Set α}
[ConditionallyCompleteLinearOrder α]
[OrderTop α]
[OrderBot α]
[LocallyFiniteOrder α]
(h₀ : I.Nonempty)
:
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 α]
: