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.
It suffices to prove [[x, y]] ⊆ s for x y ∈ s, x ≤ y.
theorem
Set.ordConnected_of_Ioo
{α : Type u_3}
[PartialOrder α]
{s : Set α}
(hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s)
:
theorem
Set.OrdConnected.preimage_mono
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{s : Set α}
{f : β → α}
(hs : s.OrdConnected)
(hf : Monotone f)
:
(f ⁻¹' s).OrdConnected
theorem
Set.OrdConnected.preimage_anti
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{s : Set α}
{f : β → α}
(hs : s.OrdConnected)
(hf : Antitone f)
:
(f ⁻¹' s).OrdConnected
theorem
Set.Icc_subset
{α : Type u_1}
[Preorder α]
(s : Set α)
[hs : s.OrdConnected]
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s)
:
@[simp]
theorem
Set.image_subtype_val_Icc
{α : Type u_1}
[Preorder α]
{s : Set α}
[s.OrdConnected]
(x y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ico
{α : Type u_1}
[Preorder α]
{s : Set α}
[s.OrdConnected]
(x y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ioc
{α : Type u_1}
[Preorder α]
{s : Set α}
[s.OrdConnected]
(x y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ioo
{α : Type u_1}
[Preorder α]
{s : Set α}
[s.OrdConnected]
(x y : ↑s)
:
theorem
Set.OrdConnected.inter
{α : Type u_1}
[Preorder α]
{s t : Set α}
(hs : s.OrdConnected)
(ht : t.OrdConnected)
:
(s ∩ t).OrdConnected
instance
Set.OrdConnected.inter'
{α : Type u_1}
[Preorder α]
{s t : Set α}
[s.OrdConnected]
[t.OrdConnected]
:
(s ∩ t).OrdConnected
theorem
Set.ordConnected_sInter
{α : Type u_1}
[Preorder α]
{S : Set (Set α)}
(hS : ∀ s ∈ S, s.OrdConnected)
:
(⋂₀ S).OrdConnected
theorem
Set.ordConnected_iInter
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{s : ι → Set α}
(hs : ∀ (i : ι), (s i).OrdConnected)
:
(⋂ (i : ι), s i).OrdConnected
instance
Set.ordConnected_iInter'
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{s : ι → Set α}
[∀ (i : ι), (s i).OrdConnected]
:
(⋂ (i : ι), s i).OrdConnected
theorem
Set.ordConnected_biInter
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{p : ι → Prop}
{s : (i : ι) → p i → Set α}
(hs : ∀ (i : ι) (hi : p i), (s i hi).OrdConnected)
:
(⋂ (i : ι), ⋂ (hi : p i), s i hi).OrdConnected
theorem
Set.ordConnected_pi
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
(h : ∀ i ∈ s, (t i).OrdConnected)
:
(s.pi t).OrdConnected
instance
Set.ordConnected_pi'
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
[h : ∀ (i : ι), (t i).OrdConnected]
:
(s.pi t).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_preimage
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{F : Type u_3}
[FunLike F α β]
[OrderHomClass F α β]
(f : F)
{s : Set β}
[hs : s.OrdConnected]
:
(⇑f ⁻¹' s).OrdConnected
instance
Set.ordConnected_image
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{E : Type u_3}
[EquivLike E α β]
[OrderIsoClass E α β]
(e : E)
{s : Set α}
[hs : s.OrdConnected]
:
(⇑e '' s).OrdConnected
instance
Set.ordConnected_range
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{E : Type u_3}
[EquivLike E α β]
[OrderIsoClass E α β]
(e : E)
:
(range ⇑e).OrdConnected
@[simp]
theorem
Set.OrdConnected.preimage_monotoneOn
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : β → α}
{t : Set β}
{s : Set α}
(hs : s.OrdConnected)
(hf : MonotoneOn f t)
:
The preimage of an OrdConnected set under a map which is monotone on a set t,
when intersected with t, is OrdConnected. More precisely, it is the intersection with t
of an OrdConnected set.
theorem
Set.OrdConnected.preimage_antitoneOn
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : β → α}
{t : Set β}
{s : Set α}
(hs : s.OrdConnected)
(hf : AntitoneOn f t)
:
The preimage of an OrdConnected set under a map which is antitone on a set t,
when intersected with t, is OrdConnected. More precisely, it is the intersection with t
of an OrdConnected set.
theorem
IsAntichain.ordConnected
{α : Type u_1}
[PartialOrder α]
{s : Set α}
(hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
Set.ordConnected_inter_Icc_of_subset
{α : Type u_1}
[PartialOrder α]
{s : Set α}
{x y : α}
(h : Ioo x y ⊆ s)
:
(s ∩ Icc x y).OrdConnected
theorem
Set.ordConnected_inter_Icc_iff
{α : Type u_1}
[PartialOrder α]
{s : Set α}
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s)
:
theorem
Set.not_ordConnected_inter_Icc_iff
{α : Type u_1}
[PartialOrder α]
{s : Set α}
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s)
:
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, uIcc x y ⊆ s)
:
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)
: