Documentation

Mathlib.Order.Interval.Set.OrdConnectedComponent

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
Instances For
theorem Set.mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} :
theorem Set.ordConnectedComponent_subset {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
theorem Set.subset_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {t : Set α} [h : s.OrdConnected] (hs : x s) (ht : s t) :
@[simp]
theorem Set.self_mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
@[simp]
theorem Set.nonempty_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
@[simp]
theorem Set.ordConnectedComponent_eq_empty {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
theorem Set.mem_ordConnectedComponent_trans {α : Type u_1} [LinearOrder α] {s : Set α} {x y z : α} (hxy : y s.ordConnectedComponent x) (hyz : z s.ordConnectedComponent y) :
theorem Set.ordConnectedComponent_eq {α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} (h : uIcc x y s) :
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
@[simp]
theorem Set.ordConnectedProj_eq {α : Type u_1} [LinearOrder α] {s : Set α} {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
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 : 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
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
theorem Set.disjoint_ordT5Nhd {α : Type u_1} [LinearOrder α] {s t : Set α} :