Order-connected sets #
We say that a set s : Set α is OrdConnected if for all x y ∈ s it includes the
interval [[x, y]]. If α is a DenselyOrdered ConditionallyCompleteLinearOrder with
the OrderTopology, then this condition is equivalent to IsPreconnected s. If α is a
LinearOrderedField, then this condition is also equivalent to Convex α s.
In this file we prove that intersection of a family of OrdConnected sets is OrdConnected and
that all standard intervals are OrdConnected.
theorem
Set.ordConnected_of_Ioo
{α : Type u_3}
[PartialOrder α]
{s : Set α}
(hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Set.Ioo x y ⊆ s)
:
s.OrdConnected
instance
Set.instDenselyOrdered
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{s : Set α}
[hs : s.OrdConnected]
:
In a dense order α, the subtype from an OrdConnected set is also densely ordered.
instance
Set.ordConnected_range
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{E : Type u_3}
[EquivLike E α β]
[OrderIsoClass E α β]
(e : E)
:
(Set.range ⇑e).OrdConnected
theorem
IsAntichain.ordConnected
{α : Type u_1}
[PartialOrder α]
{s : Set α}
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
s.OrdConnected
theorem
Set.ordConnected_inter_Icc_of_subset
{α : Type u_1}
[PartialOrder α]
{s : Set α}
{x y : α}
(h : Set.Ioo x y ⊆ s)
:
instance
Set.ordConnected_uIcc
{α : Type u_1}
[LinearOrder α]
{a b : α}
:
(Set.uIcc a b).OrdConnected
theorem
Set.OrdConnected.uIcc_subset
{α : Type u_1}
[LinearOrder α]
{s : Set α}
(hs : s.OrdConnected)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s)
:
theorem
Set.OrdConnected.uIoc_subset
{α : Type u_1}
[LinearOrder α]
{s : Set α}
(hs : s.OrdConnected)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s)
:
theorem
Set.ordConnected_of_uIcc_subset_left
{α : Type u_1}
[LinearOrder α]
{s : Set α}
{x : α}
(h : ∀ y ∈ s, Set.uIcc x y ⊆ s)
:
s.OrdConnected
theorem
Set.ordConnected_iff_uIcc_subset_left
{α : Type u_1}
[LinearOrder α]
{s : Set α}
{x : α}
(hx : x ∈ s)
:
theorem
Set.ordConnected_iff_uIcc_subset_right
{α : Type u_1}
[LinearOrder α]
{s : Set α}
{x : α}
(hx : x ∈ s)
: