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.
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.
s : Set αisOrdConnectedif for allx y ∈ sit includes the interval[[x, y]].
Instances
theorem
Set.OrdConnected.out
{α : Type u_1}
[Preorder α]
{s : Set α}
(h : Set.OrdConnected s)
⦃x : α⦄
:
theorem
Set.ordConnected_iff
{α : Type u_1}
[Preorder α]
{s : Set α}
:
Set.OrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Set.Icc x y ⊆ s
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 → Set.Ioo x y ⊆ s)
:
theorem
Set.OrdConnected.preimage_mono
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{s : Set α}
{f : β → α}
(hs : Set.OrdConnected s)
(hf : Monotone f)
:
Set.OrdConnected (f ⁻¹' s)
theorem
Set.OrdConnected.preimage_anti
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{s : Set α}
{f : β → α}
(hs : Set.OrdConnected s)
(hf : Antitone f)
:
Set.OrdConnected (f ⁻¹' s)
theorem
Set.Icc_subset
{α : Type u_1}
[Preorder α]
(s : Set α)
[hs : Set.OrdConnected s]
{x : α}
{y : α}
(hx : x ∈ s)
(hy : y ∈ s)
:
@[simp]
theorem
Set.image_subtype_val_Icc
{α : Type u_1}
[Preorder α]
{s : Set α}
[Set.OrdConnected s]
(x : ↑s)
(y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ico
{α : Type u_1}
[Preorder α]
{s : Set α}
[Set.OrdConnected s]
(x : ↑s)
(y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ioc
{α : Type u_1}
[Preorder α]
{s : Set α}
[Set.OrdConnected s]
(x : ↑s)
(y : ↑s)
:
@[simp]
theorem
Set.image_subtype_val_Ioo
{α : Type u_1}
[Preorder α]
{s : Set α}
[Set.OrdConnected s]
(x : ↑s)
(y : ↑s)
:
theorem
Set.OrdConnected.inter
{α : Type u_1}
[Preorder α]
{s : Set α}
{t : Set α}
(hs : Set.OrdConnected s)
(ht : Set.OrdConnected t)
:
Set.OrdConnected (s ∩ t)
instance
Set.OrdConnected.inter'
{α : Type u_1}
[Preorder α]
{s : Set α}
{t : Set α}
[Set.OrdConnected s]
[Set.OrdConnected t]
:
Set.OrdConnected (s ∩ t)
Equations
- (_ : Set.OrdConnected (s ∩ t)) = (_ : Set.OrdConnected (s ∩ t))
theorem
Set.OrdConnected.dual
{α : Type u_1}
[Preorder α]
{s : Set α}
(hs : Set.OrdConnected s)
:
Set.OrdConnected (⇑OrderDual.ofDual ⁻¹' s)
theorem
Set.ordConnected_dual
{α : Type u_1}
[Preorder α]
{s : Set α}
:
Set.OrdConnected (⇑OrderDual.ofDual ⁻¹' s) ↔ Set.OrdConnected s
theorem
Set.ordConnected_sInter
{α : Type u_1}
[Preorder α]
{S : Set (Set α)}
(hS : ∀ s ∈ S, Set.OrdConnected s)
:
Set.OrdConnected (⋂₀ S)
theorem
Set.ordConnected_iInter
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{s : ι → Set α}
(hs : ∀ (i : ι), Set.OrdConnected (s i))
:
Set.OrdConnected (⋂ (i : ι), s i)
instance
Set.ordConnected_iInter'
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{s : ι → Set α}
[∀ (i : ι), Set.OrdConnected (s i)]
:
Set.OrdConnected (⋂ (i : ι), s i)
Equations
- (_ : Set.OrdConnected (⋂ (i : ι), s i)) = (_ : Set.OrdConnected (⋂ (i : ι), s i))
theorem
Set.ordConnected_biInter
{α : Type u_1}
[Preorder α]
{ι : Sort u_3}
{p : ι → Prop}
{s : (i : ι) → p i → Set α}
(hs : ∀ (i : ι) (hi : p i), Set.OrdConnected (s i hi))
:
Set.OrdConnected (⋂ (i : ι), ⋂ (hi : p i), s i hi)
theorem
Set.ordConnected_pi
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
(h : ∀ i ∈ s, Set.OrdConnected (t i))
:
Set.OrdConnected (Set.pi s t)
instance
Set.ordConnected_pi'
{ι : Type u_3}
{α : ι → Type u_4}
[(i : ι) → Preorder (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
[h : ∀ (i : ι), Set.OrdConnected (t i)]
:
Set.OrdConnected (Set.pi s t)
Equations
- (_ : Set.OrdConnected (Set.pi s t)) = (_ : Set.OrdConnected (Set.pi s t))
theorem
Set.ordConnected_Icc
{α : Type u_1}
[Preorder α]
{a : α}
{b : α}
:
Set.OrdConnected (Set.Icc a b)
theorem
Set.ordConnected_Ico
{α : Type u_1}
[Preorder α]
{a : α}
{b : α}
:
Set.OrdConnected (Set.Ico a b)
theorem
Set.ordConnected_Ioc
{α : Type u_1}
[Preorder α]
{a : α}
{b : α}
:
Set.OrdConnected (Set.Ioc a b)
theorem
Set.ordConnected_Ioo
{α : Type u_1}
[Preorder α]
{a : α}
{b : α}
:
Set.OrdConnected (Set.Ioo a b)
instance
Set.instDenselyOrdered
{α : Type u_1}
[Preorder α]
[DenselyOrdered α]
{s : Set α}
[hs : Set.OrdConnected s]
:
In a dense order α, the subtype from an OrdConnected set is also densely ordered.
Equations
- (_ : DenselyOrdered ↑s) = (_ : DenselyOrdered ↑s)
theorem
Set.ordConnected_preimage
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{F : Type u_3}
[FunLike F α β]
[OrderHomClass F α β]
(f : F)
{s : Set β}
[hs : Set.OrdConnected s]
:
Set.OrdConnected (⇑f ⁻¹' s)
theorem
Set.ordConnected_image
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{E : Type u_3}
[EquivLike E α β]
[OrderIsoClass E α β]
(e : E)
{s : Set α}
[hs : Set.OrdConnected s]
:
Set.OrdConnected (⇑e '' s)
theorem
Set.ordConnected_range
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{E : Type u_3}
[EquivLike E α β]
[OrderIsoClass E α β]
(e : E)
:
@[simp]
theorem
Set.dual_ordConnected_iff
{α : Type u_1}
[Preorder α]
{s : Set α}
:
Set.OrdConnected (⇑OrderDual.ofDual ⁻¹' s) ↔ Set.OrdConnected s
theorem
Set.dual_ordConnected
{α : Type u_1}
[Preorder α]
{s : Set α}
[Set.OrdConnected s]
:
Set.OrdConnected (⇑OrderDual.ofDual ⁻¹' s)
theorem
IsAntichain.ordConnected
{α : Type u_1}
[PartialOrder α]
{s : Set α}
(hs : IsAntichain (fun (x x_1 : α) => x ≤ x_1) s)
:
theorem
Set.ordConnected_uIcc
{α : Type u_1}
[LinearOrder α]
{a : α}
{b : α}
:
Set.OrdConnected (Set.uIcc a b)
theorem
Set.ordConnected_uIoc
{α : Type u_1}
[LinearOrder α]
{a : α}
{b : α}
:
Set.OrdConnected (Ι a b)
theorem
Set.OrdConnected.uIcc_subset
{α : Type u_1}
[LinearOrder α]
{s : Set α}
(hs : Set.OrdConnected s)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s)
:
theorem
Set.OrdConnected.uIoc_subset
{α : Type u_1}
[LinearOrder α]
{s : Set α}
(hs : Set.OrdConnected s)
⦃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)
:
theorem
Set.ordConnected_iff_uIcc_subset_left
{α : Type u_1}
[LinearOrder α]
{s : Set α}
{x : α}
(hx : x ∈ s)
:
Set.OrdConnected s ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
theorem
Set.ordConnected_iff_uIcc_subset_right
{α : Type u_1}
[LinearOrder α]
{s : Set α}
{x : α}
(hx : x ∈ s)
:
Set.OrdConnected s ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc y x ⊆ s