Documentation

Mathlib.Data.Set.Intervals.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⊆ 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} [inst : 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⊆ s. Note that it is empty if and only if x ∉ s∉ s.

Equations

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

theorem Set.mem_ordConnectedComponent {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} {y : α} :

y ∈ Set.ordConnectedComponent s x ↔ Set.uIcc x y ⊆ s

theorem Set.dual_ordConnectedComponent {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} :

Set.ordConnectedComponent (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.toDual x) = ↑OrderDual.ofDual ⁻¹' Set.ordConnectedComponent s x

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

Set.ordConnectedComponent s x ⊆ s

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

s ⊆ Set.ordConnectedComponent t x

@[simp]

theorem Set.self_mem_ordConnectedComponent {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} :

x ∈ Set.ordConnectedComponent s x ↔ x ∈ s

@[simp]

theorem Set.nonempty_ordConnectedComponent {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} :

Set.Nonempty (Set.ordConnectedComponent s x) ↔ x ∈ s

@[simp]

theorem Set.ordConnectedComponent_eq_empty {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} :

Set.ordConnectedComponent s x = ∅ ↔ ¬x ∈ s

@[simp]

theorem Set.ordConnectedComponent_empty {α : Type u_1} [inst : LinearOrder α] {x : α} :

Set.ordConnectedComponent ∅ x = ∅

@[simp]

theorem Set.ordConnectedComponent_univ {α : Type u_1} [inst : LinearOrder α] {x : α} :

Set.ordConnectedComponent Set.univ x = Set.univ

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

Set.ordConnectedComponent (s ∩ t) x = Set.ordConnectedComponent s x ∩ Set.ordConnectedComponent t x

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

y ∈ Set.ordConnectedComponent s x ↔ x ∈ Set.ordConnectedComponent s y

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

z ∈ Set.ordConnectedComponent s x

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

Set.ordConnectedComponent s x = Set.ordConnectedComponent s y

instance Set.instOrdConnectedToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeOrdConnectedComponent {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} :

Set.OrdConnected (Set.ordConnectedComponent s x)

Equations

One or more equations did not get rendered due to their size.

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

↑s → α

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

Equations

Set.ordConnectedProj s x = Set.Nonempty.some (_ : Set.Nonempty (Set.ordConnectedComponent s ↑x))

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

Set.ordConnectedProj s x ∈ Set.ordConnectedComponent s ↑x

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

↑x ∈ Set.ordConnectedComponent s (Set.ordConnectedProj s x)

@[simp]

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

Set.ordConnectedComponent s (Set.ordConnectedProj s x) = Set.ordConnectedComponent s ↑x

@[simp]

theorem Set.ordConnectedProj_eq {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : ↑s} {y : ↑s} :

Set.ordConnectedProj s x = Set.ordConnectedProj s y ↔ Set.uIcc ↑x ↑y ⊆ s

def Set.ordConnectedSection {α : Type u_1} [inst : 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

Set.ordConnectedSection s = Set.range (Set.ordConnectedProj s)

theorem Set.dual_ordConnectedSection {α : Type u_1} [inst : LinearOrder α] (s : Set α) :

Set.ordConnectedSection (↑OrderDual.ofDual ⁻¹' s) = ↑OrderDual.ofDual ⁻¹' Set.ordConnectedSection s

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

Set.ordConnectedSection s ⊆ s

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

x = y

def Set.ordSeparatingSet {α : Type u_1} [inst : LinearOrder α] (s : Set α) (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∈ s, and to some Set.ordConnectedComponent sᶜ x, x ∈ t∈ 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

Set.ordSeparatingSet s t = (Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (tᶜ) x) ∩ Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (sᶜ) x

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

Set.ordSeparatingSet s t = Set.ordSeparatingSet t s

theorem Set.disjoint_left_ordSeparatingSet {α : Type u_1} [inst : LinearOrder α] {s : Set α} {t : Set α} :

Disjoint s (Set.ordSeparatingSet s t)

theorem Set.disjoint_right_ordSeparatingSet {α : Type u_1} [inst : LinearOrder α] {s : Set α} {t : Set α} :

Disjoint t (Set.ordSeparatingSet s t)

theorem Set.dual_ordSeparatingSet {α : Type u_1} [inst : LinearOrder α] {s : Set α} {t : Set α} :

Set.ordSeparatingSet (↑OrderDual.ofDual ⁻¹' s) (↑OrderDual.ofDual ⁻¹' t) = ↑OrderDual.ofDual ⁻¹' Set.ordSeparatingSet s t

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

Set α

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

Equations

Set.ordT5Nhd s t = Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (tᶜ ∩ Set.ordConnectedSection (Set.ordSeparatingSet s t)ᶜ) x

theorem Set.disjoint_ordT5Nhd {α : Type u_1} [inst : LinearOrder α] {s : Set α} {t : Set α} :

Disjoint (Set.ordT5Nhd s t) (Set.ordT5Nhd t s)