Order connected components of a set

In this file we define Set.ordConnectedComponent s x to be the set of y such that Set.uIcc x y ⊆ s and prove some basic facts about this definition. At the moment of writing, this construction is used only to prove that any linear order with order topology is a T₅ space, so we only add API needed for this lemma.

def Set.ordConnectedComponent {α : Type u_1} [LinearOrder α] (s : Set α) (x : α) : Set α

Order-connected component of a point x in a set s. It is defined as the set of y such that Set.uIcc x y ⊆ s. Note that it is empty if and only if x ∉ s.

Equations

• s.ordConnectedComponent x = {y : α | Set.uIcc x y ⊆ s}

theorem Set.mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} : y ∈ s.ordConnectedComponent x ↔ Set.uIcc x y ⊆ s

theorem Set.dual_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : (⇑OrderDual.ofDual ⁻¹' s).ordConnectedComponent (OrderDual.toDual x) = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedComponent x

theorem Set.ordConnectedComponent_subset {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : s.ordConnectedComponent x ⊆ s

theorem Set.subset_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {t : Set α} [h : s.OrdConnected] (hs : x ∈ s) (ht : s ⊆ t) : s ⊆ t.ordConnectedComponent x

@[simp]

theorem Set.self_mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : x ∈ s.ordConnectedComponent x ↔ x ∈ s

@[simp]

theorem Set.nonempty_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : (s.ordConnectedComponent x).Nonempty ↔ x ∈ s

@[simp]

theorem Set.ordConnectedComponent_eq_empty {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : s.ordConnectedComponent x = ∅ ↔ x ∉ s

@[simp]

theorem Set.ordConnectedComponent_empty {α : Type u_1} [LinearOrder α] {x : α} : ∅.ordConnectedComponent x = ∅

@[simp]

theorem Set.ordConnectedComponent_univ {α : Type u_1} [LinearOrder α] {x : α} : Set.univ.ordConnectedComponent x = Set.univ

theorem Set.ordConnectedComponent_inter {α : Type u_1} [LinearOrder α] (s t : Set α) (x : α) : (s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x

theorem Set.mem_ordConnectedComponent_comm {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} : y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y

theorem Set.mem_ordConnectedComponent_trans {α : Type u_1} [LinearOrder α] {s : Set α} {x y z : α} (hxy : y ∈ s.ordConnectedComponent x) (hyz : z ∈ s.ordConnectedComponent y) : z ∈ s.ordConnectedComponent x

theorem Set.ordConnectedComponent_eq {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} (h : Set.uIcc x y ⊆ s) : s.ordConnectedComponent x = s.ordConnectedComponent y

instance Set.instOrdConnectedOrdConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} : (s.ordConnectedComponent x).OrdConnected

Equations

• ⋯ = ⋯

noncomputable def Set.ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) : ↑s → α

Projection from s : Set α to α sending each order connected component of s to a single point of this component.

Equations

• s.ordConnectedProj x = ⋯.some

theorem Set.ordConnectedProj_mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] (s : Set α) (x : ↑s) : s.ordConnectedProj x ∈ s.ordConnectedComponent ↑x

theorem Set.mem_ordConnectedComponent_ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) (x : ↑s) : ↑x ∈ s.ordConnectedComponent (s.ordConnectedProj x)

@[simp]

theorem Set.ordConnectedComponent_ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) (x : ↑s) : s.ordConnectedComponent (s.ordConnectedProj x) = s.ordConnectedComponent ↑x

@[simp]

theorem Set.ordConnectedProj_eq {α : Type u_1} [LinearOrder α] {s : Set α} {x y : ↑s} : s.ordConnectedProj x = s.ordConnectedProj y ↔ Set.uIcc ↑x ↑y ⊆ s

def Set.ordConnectedSection {α : Type u_1} [LinearOrder α] (s : Set α) : Set α

A set that intersects each order connected component of a set by a single point. Defined as the range of Set.ordConnectedProj s.

Equations

• s.ordConnectedSection = Set.range s.ordConnectedProj

theorem Set.dual_ordConnectedSection {α : Type u_1} [LinearOrder α] (s : Set α) : (⇑OrderDual.ofDual ⁻¹' s).ordConnectedSection = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedSection

theorem Set.ordConnectedSection_subset {α : Type u_1} [LinearOrder α] {s : Set α} : s.ordConnectedSection ⊆ s

theorem Set.eq_of_mem_ordConnectedSection_of_uIcc_subset {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} (hx : x ∈ s.ordConnectedSection) (hy : y ∈ s.ordConnectedSection) (h : Set.uIcc x y ⊆ s) : x = y

def Set.ordSeparatingSet {α : Type u_1} [LinearOrder α] (s t : Set α) : Set α

Given two sets s t : Set α, the set Set.orderSeparatingSet s t is the set of points that belong both to some Set.ordConnectedComponent tᶜ x, x ∈ s, and to some Set.ordConnectedComponent sᶜ x, x ∈ t. In the case of two disjoint closed sets, this is the union of all open intervals $(a, b)$ such that their endpoints belong to different sets.

Equations

• s.ordSeparatingSet t = (⋃ x ∈ s, tᶜ.ordConnectedComponent x) ∩ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

theorem Set.ordSeparatingSet_comm {α : Type u_1} [LinearOrder α] (s t : Set α) : s.ordSeparatingSet t = t.ordSeparatingSet s

theorem Set.disjoint_left_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s t : Set α} : Disjoint s (s.ordSeparatingSet t)

theorem Set.disjoint_right_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s t : Set α} : Disjoint t (s.ordSeparatingSet t)

theorem Set.dual_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s t : Set α} : (⇑OrderDual.ofDual ⁻¹' s).ordSeparatingSet (⇑OrderDual.ofDual ⁻¹' t) = ⇑OrderDual.ofDual ⁻¹' s.ordSeparatingSet t

def Set.ordT5Nhd {α : Type u_1} [LinearOrder α] (s t : Set α) : Set α

An auxiliary neighborhood that will be used in the proof of OrderTopology.CompletelyNormalSpace.

Equations

• s.ordT5Nhd t = ⋃ x ∈ s, (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent x

theorem Set.disjoint_ordT5Nhd {α : Type u_1} [LinearOrder α] {s t : Set α} : Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)