# Documentation

Mathlib.Data.Set.Intervals.OrdConnected

# 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.

class Set.OrdConnected {α : Type u_1} [] (s : Set α) :
• out' : ∀ ⦃x : α⦄, x s✝∀ ⦃y : α⦄, y s✝Set.Icc x y s✝

s : Set α is OrdConnected if for all x y ∈ s it includes the interval [[x, y]].

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.

Instances
theorem Set.OrdConnected.out {α : Type u_1} [] {s : Set α} (h : ) ⦃x : α :
x s∀ ⦃y : α⦄, y sSet.Icc x y s
theorem Set.ordConnected_def {α : Type u_1} [] {s : Set α} :
∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sSet.Icc x y s
theorem Set.ordConnected_iff {α : Type u_1} [] {s : Set α} :
∀ (x : α), x s∀ (y : α), y sx ySet.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} [] {s : Set α} (hs : ∀ (x : α), x s∀ (y : α), y sx < ySet.Ioo x y s) :
theorem Set.OrdConnected.preimage_mono {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {f : βα} (hs : ) (hf : ) :
theorem Set.OrdConnected.preimage_anti {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {f : βα} (hs : ) (hf : ) :
theorem Set.Icc_subset {α : Type u_1} [] (s : Set α) [hs : ] {x : α} {y : α} (hx : x s) (hy : y s) :
Set.Icc x y s
theorem Set.OrdConnected.inter {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
instance Set.OrdConnected.inter' {α : Type u_1} [] {s : Set α} {t : Set α} [] [] :
theorem Set.OrdConnected.dual {α : Type u_1} [] {s : Set α} (hs : ) :
Set.OrdConnected (OrderDual.ofDual ⁻¹' s)
theorem Set.ordConnected_dual {α : Type u_1} [] {s : Set α} :
Set.OrdConnected (OrderDual.ofDual ⁻¹' s)
theorem Set.ordConnected_sInter {α : Type u_1} [] {S : Set (Set α)} (hS : ∀ (s : Set α), s S) :
theorem Set.ordConnected_iInter {α : Type u_1} [] {ι : Sort u_3} {s : ιSet α} (hs : ∀ (i : ι), Set.OrdConnected (s i)) :
Set.OrdConnected (⋂ (i : ι), s i)
instance Set.ordConnected_iInter' {α : Type u_1} [] {ι : Sort u_3} {s : ιSet α} [∀ (i : ι), Set.OrdConnected (s i)] :
Set.OrdConnected (⋂ (i : ι), s i)
theorem Set.ordConnected_biInter {α : Type u_1} [] {ι : Sort u_3} {p : ιProp} {s : (i : ι) → p iSet α} (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 : ι), i sSet.OrdConnected (t i)) :
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)] :
theorem Set.ordConnected_Ici {α : Type u_1} [] {a : α} :
theorem Set.ordConnected_Iic {α : Type u_1} [] {a : α} :
theorem Set.ordConnected_Ioi {α : Type u_1} [] {a : α} :
theorem Set.ordConnected_Iio {α : Type u_1} [] {a : α} :
theorem Set.ordConnected_Icc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.ordConnected_Ico {α : Type u_1} [] {a : α} {b : α} :
theorem Set.ordConnected_Ioc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.ordConnected_Ioo {α : Type u_1} [] {a : α} {b : α} :
theorem Set.ordConnected_singleton {α : Type u_3} [] {a : α} :
theorem Set.ordConnected_empty {α : Type u_1} [] :
theorem Set.ordConnected_univ {α : Type u_1} [] :
instance Set.instDenselyOrdered {α : Type u_1} [] [] {s : Set α} [hs : ] :

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

theorem Set.ordConnected_preimage {α : Type u_1} {β : Type u_2} [] [] {F : Type u_3} [] (f : F) {s : Set β} [hs : ] :
theorem Set.ordConnected_image {α : Type u_1} {β : Type u_2} [] [] {E : Type u_3} [] (e : E) {s : Set α} [hs : ] :
theorem Set.ordConnected_range {α : Type u_1} {β : Type u_2} [] [] {E : Type u_3} [] (e : E) :
@[simp]
theorem Set.dual_ordConnected_iff {α : Type u_1} [] {s : Set α} :
Set.OrdConnected (OrderDual.ofDual ⁻¹' s)
theorem Set.dual_ordConnected {α : Type u_1} [] {s : Set α} [] :
Set.OrdConnected (OrderDual.ofDual ⁻¹' s)
theorem IsAntichain.ordConnected {α : Type u_1} [] {s : Set α} (hs : IsAntichain (fun x x_1 => x x_1) s) :
theorem Set.ordConnected_uIcc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.ordConnected_uIoc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.OrdConnected.uIcc_subset {α : Type u_1} [] {s : Set α} (hs : ) ⦃x : α (hx : x s) ⦃y : α (hy : y s) :
theorem Set.OrdConnected.uIoc_subset {α : Type u_1} [] {s : Set α} (hs : ) ⦃x : α (hx : x s) ⦃y : α (hy : y s) :
Ι x y s
theorem Set.ordConnected_iff_uIcc_subset {α : Type u_1} [] {s : Set α} :
∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sSet.uIcc x y s
theorem Set.ordConnected_of_uIcc_subset_left {α : Type u_1} [] {s : Set α} {x : α} (h : ∀ (y : α), y sSet.uIcc x y s) :
theorem Set.ordConnected_iff_uIcc_subset_left {α : Type u_1} [] {s : Set α} {x : α} (hx : x s) :
∀ ⦃y : α⦄, y sSet.uIcc x y s
theorem Set.ordConnected_iff_uIcc_subset_right {α : Type u_1} [] {s : Set α} {x : α} (hx : x s) :
∀ ⦃y : α⦄, y sSet.uIcc y x s