mathlib3documentation

data.set.intervals.ord_connected_component

Order connected components of a set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define set.ord_connected_component 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.ord_connected_component {α : Type u_1} [linear_order α] (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
• = {y : α | y s}
Instances for set.ord_connected_component
theorem set.mem_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x y : α} :
y s
theorem set.dual_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :
theorem set.ord_connected_component_subset {α : Type u_1} [linear_order α] {s : set α} {x : α} :
theorem set.subset_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} {t : set α} [h : s.ord_connected] (hs : x s) (ht : s t) :
@[simp]
theorem set.self_mem_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :
x s
@[simp]
theorem set.nonempty_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :
x s
@[simp]
theorem set.ord_connected_component_eq_empty {α : Type u_1} [linear_order α] {s : set α} {x : α} :
x s
@[simp]
theorem set.ord_connected_component_empty {α : Type u_1} [linear_order α] {x : α} :
@[simp]
theorem set.ord_connected_component_univ {α : Type u_1} [linear_order α] {x : α} :
theorem set.ord_connected_component_inter {α : Type u_1} [linear_order α] (s t : set α) (x : α) :
theorem set.mem_ord_connected_component_comm {α : Type u_1} [linear_order α] {s : set α} {x y : α} :
theorem set.mem_ord_connected_component_trans {α : Type u_1} [linear_order α] {s : set α} {x y z : α} (hxy : y ) (hyz : z ) :
theorem set.ord_connected_component_eq {α : Type u_1} [linear_order α] {s : set α} {x y : α} (h : y s) :
@[protected, instance]
def set.ord_connected_component.ord_connected {α : Type u_1} [linear_order α] {s : set α} {x : α} :
noncomputable def set.ord_connected_proj {α : Type u_1} [linear_order α] (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.ord_connected_component_ord_connected_proj {α : Type u_1} [linear_order α] (s : set α) (x : s) :
@[simp]
theorem set.ord_connected_proj_eq {α : Type u_1} [linear_order α] {s : set α} {x y : s} :
y s
def set.ord_connected_section {α : Type u_1} [linear_order α] (s : set α) :
set α

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

Equations
theorem set.dual_ord_connected_section {α : Type u_1} [linear_order α] (s : set α) :
theorem set.ord_connected_section_subset {α : Type u_1} [linear_order α] {s : set α} :
theorem set.eq_of_mem_ord_connected_section_of_uIcc_subset {α : Type u_1} [linear_order α] {s : set α} {x y : α} (hx : x s.ord_connected_section) (hy : y s.ord_connected_section) (h : y s) :
x = y
def set.ord_separating_set {α : Type u_1} [linear_order α] (s t : set α) :
set α

Given two sets s t : set α, the set set.order_separating_set s t is the set of points that belong both to some set.ord_connected_component tᶜ x, x ∈ s, and to some set.ord_connected_component 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
theorem set.ord_separating_set_comm {α : Type u_1} [linear_order α] (s t : set α) :
theorem set.dual_ord_separating_set {α : Type u_1} [linear_order α] {s t : set α} :
def set.ord_t5_nhd {α : Type u_1} [linear_order α] (s t : set α) :
set α

An auxiliary neighborhood that will be used in the proof of order_topology.t5_space.

Equations
theorem set.disjoint_ord_t5_nhd {α : Type u_1} [linear_order α] {s t : set α} :