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.out {α : Type u_1} [Preorder α] {s : Set α} (h : s.OrdConnected) ⦃x : α⦄ : x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s

theorem Set.ordConnected_def {α : Type u_1} [Preorder α] {s : Set α} : s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s

theorem Set.ordConnected_iff {α : Type u_1} [Preorder α] {s : Set α} : s.OrdConnected ↔ ∀ 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) : s.OrdConnected

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) : Set.Icc x y ⊆ s

theorem OrderEmbedding.image_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : (Set.range ⇑e).OrdConnected) (x : α) (y : α) : ⇑e '' Set.Icc x y = Set.Icc (e x) (e y)

theorem OrderEmbedding.image_Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : (Set.range ⇑e).OrdConnected) (x : α) (y : α) : ⇑e '' Set.Ico x y = Set.Ico (e x) (e y)

theorem OrderEmbedding.image_Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : (Set.range ⇑e).OrdConnected) (x : α) (y : α) : ⇑e '' Set.Ioc x y = Set.Ioc (e x) (e y)

theorem OrderEmbedding.image_Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : (Set.range ⇑e).OrdConnected) (x : α) (y : α) : ⇑e '' Set.Ioo x y = Set.Ioo (e x) (e y)

@[simp]

theorem Set.image_subtype_val_Icc {α : Type u_1} [Preorder α] {s : Set α} [s.OrdConnected] (x : ↑s) (y : ↑s) : Subtype.val '' Set.Icc x y = Set.Icc ↑x ↑y

@[simp]

theorem Set.image_subtype_val_Ico {α : Type u_1} [Preorder α] {s : Set α} [s.OrdConnected] (x : ↑s) (y : ↑s) : Subtype.val '' Set.Ico x y = Set.Ico ↑x ↑y

@[simp]

theorem Set.image_subtype_val_Ioc {α : Type u_1} [Preorder α] {s : Set α} [s.OrdConnected] (x : ↑s) (y : ↑s) : Subtype.val '' Set.Ioc x y = Set.Ioc ↑x ↑y

@[simp]

theorem Set.image_subtype_val_Ioo {α : Type u_1} [Preorder α] {s : Set α} [s.OrdConnected] (x : ↑s) (y : ↑s) : Subtype.val '' Set.Ioo x y = Set.Ioo ↑x ↑y

theorem Set.OrdConnected.inter {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (hs : s.OrdConnected) (ht : t.OrdConnected) : (s ∩ t).OrdConnected

instance Set.OrdConnected.inter' {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} [s.OrdConnected] [t.OrdConnected] : (s ∩ t).OrdConnected

Equations

• ⋯ = ⋯

theorem Set.OrdConnected.dual {α : Type u_1} [Preorder α] {s : Set α} (hs : s.OrdConnected) : (⇑OrderDual.ofDual ⁻¹' s).OrdConnected

theorem Set.ordConnected_dual {α : Type u_1} [Preorder α] {s : Set α} : (⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Set.ordConnected_Ici {α : Type u_1} [Preorder α] {a : α} : (Set.Ici a).OrdConnected

theorem Set.ordConnected_Iic {α : Type u_1} [Preorder α] {a : α} : (Set.Iic a).OrdConnected

theorem Set.ordConnected_Ioi {α : Type u_1} [Preorder α] {a : α} : (Set.Ioi a).OrdConnected

theorem Set.ordConnected_Iio {α : Type u_1} [Preorder α] {a : α} : (Set.Iio a).OrdConnected

theorem Set.ordConnected_Icc {α : Type u_1} [Preorder α] {a : α} {b : α} : (Set.Icc a b).OrdConnected

theorem Set.ordConnected_Ico {α : Type u_1} [Preorder α] {a : α} {b : α} : (Set.Ico a b).OrdConnected

theorem Set.ordConnected_Ioc {α : Type u_1} [Preorder α] {a : α} {b : α} : (Set.Ioc a b).OrdConnected

theorem Set.ordConnected_Ioo {α : Type u_1} [Preorder α] {a : α} {b : α} : (Set.Ioo a b).OrdConnected

theorem Set.ordConnected_singleton {α : Type u_3} [PartialOrder α] {a : α} : {a}.OrdConnected

theorem Set.ordConnected_empty {α : Type u_1} [Preorder α] : ∅.OrdConnected

theorem Set.ordConnected_univ {α : Type u_1} [Preorder α] : Set.univ.OrdConnected

instance Set.instDenselyOrdered {α : Type u_1} [Preorder α] [DenselyOrdered α] {s : Set α} [hs : s.OrdConnected] : DenselyOrdered ↑s

In a dense order α, the subtype from an OrdConnected set is also densely ordered.

Equations

• ⋯ = ⋯

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 : s.OrdConnected] : (⇑f ⁻¹' s).OrdConnected

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 : s.OrdConnected] : (⇑e '' s).OrdConnected

theorem 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

@[simp]

theorem Set.dual_ordConnected_iff {α : Type u_1} [Preorder α] {s : Set α} : (⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected

theorem Set.dual_ordConnected {α : Type u_1} [Preorder α] {s : Set α} [s.OrdConnected] : (⇑OrderDual.ofDual ⁻¹' s).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) : (s ∩ Set.Icc x y).OrdConnected

theorem Set.ordConnected_inter_Icc_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) : (s ∩ Set.Icc x y).OrdConnected ↔ Set.Ioo x y ⊆ s

theorem Set.not_ordConnected_inter_Icc_iff {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) : ¬(s ∩ Set.Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Set.Ioo x y

theorem Set.ordConnected_uIcc {α : Type u_1} [LinearOrder α] {a : α} {b : α} : (Set.uIcc a b).OrdConnected

theorem Set.ordConnected_uIoc {α : Type u_1} [LinearOrder α] {a : α} {b : α} : (Ι 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) : Set.uIcc x y ⊆ s

theorem Set.OrdConnected.uIoc_subset {α : Type u_1} [LinearOrder α] {s : Set α} (hs : s.OrdConnected) ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Ι x y ⊆ s

theorem Set.ordConnected_iff_uIcc_subset {α : Type u_1} [LinearOrder α] {s : Set α} : s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x 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) : s.OrdConnected ↔ ∀ ⦃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) : s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc y x ⊆ s