mathlib3 documentation

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

s.ord_connected_component x = {y : α | set.uIcc x y ⊆ s}

Instances for set.ord_connected_component

set.ord_connected_component.ord_connected

theorem set.mem_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x y : α} :

y ∈ s.ord_connected_component x ↔ set.uIcc x y ⊆ s

theorem set.dual_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :

(⇑order_dual.of_dual ⁻¹' s).ord_connected_component (⇑order_dual.to_dual x) = ⇑order_dual.of_dual ⁻¹' s.ord_connected_component x

theorem set.ord_connected_component_subset {α : Type u_1} [linear_order α] {s : set α} {x : α} :

s.ord_connected_component x ⊆ s

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) :

s ⊆ t.ord_connected_component x

@[simp]

theorem set.self_mem_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :

x ∈ s.ord_connected_component x ↔ x ∈ s

@[simp]

theorem set.nonempty_ord_connected_component {α : Type u_1} [linear_order α] {s : set α} {x : α} :

(s.ord_connected_component x).nonempty ↔ x ∈ s

@[simp]

theorem set.ord_connected_component_eq_empty {α : Type u_1} [linear_order α] {s : set α} {x : α} :

s.ord_connected_component x = ∅ ↔ x ∉ s

@[simp]

theorem set.ord_connected_component_empty {α : Type u_1} [linear_order α] {x : α} :

∅.ord_connected_component x = ∅

@[simp]

theorem set.ord_connected_component_univ {α : Type u_1} [linear_order α] {x : α} :

set.univ.ord_connected_component x = set.univ

theorem set.ord_connected_component_inter {α : Type u_1} [linear_order α] (s t : set α) (x : α) :

(s ∩ t).ord_connected_component x = s.ord_connected_component x ∩ t.ord_connected_component x

theorem set.mem_ord_connected_component_comm {α : Type u_1} [linear_order α] {s : set α} {x y : α} :

y ∈ s.ord_connected_component x ↔ x ∈ s.ord_connected_component y

theorem set.mem_ord_connected_component_trans {α : Type u_1} [linear_order α] {s : set α} {x y z : α} (hxy : y ∈ s.ord_connected_component x) (hyz : z ∈ s.ord_connected_component y) :

z ∈ s.ord_connected_component x

theorem set.ord_connected_component_eq {α : Type u_1} [linear_order α] {s : set α} {x y : α} (h : set.uIcc x y ⊆ s) :

s.ord_connected_component x = s.ord_connected_component y

@[protected, instance]

def set.ord_connected_component.ord_connected {α : Type u_1} [linear_order α] {s : set α} {x : α} :

(s.ord_connected_component x).ord_connected

noncomputable def set.ord_connected_proj {α : Type u_1} [linear_order α] (s : set α) :

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

Equations

s.ord_connected_proj = λ (x : ↥s), _.some

theorem set.ord_connected_proj_mem_ord_connected_component {α : Type u_1} [linear_order α] (s : set α) (x : ↥s) :

s.ord_connected_proj x ∈ s.ord_connected_component ↑x

theorem set.mem_ord_connected_component_ord_connected_proj {α : Type u_1} [linear_order α] (s : set α) (x : ↥s) :

↑x ∈ s.ord_connected_component (s.ord_connected_proj x)

@[simp]

theorem set.ord_connected_component_ord_connected_proj {α : Type u_1} [linear_order α] (s : set α) (x : ↥s) :

s.ord_connected_component (s.ord_connected_proj x) = s.ord_connected_component ↑x

@[simp]

theorem set.ord_connected_proj_eq {α : Type u_1} [linear_order α] {s : set α} {x y : ↥s} :

s.ord_connected_proj x = s.ord_connected_proj y ↔ set.uIcc ↑x ↑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

s.ord_connected_section = set.range s.ord_connected_proj

theorem set.dual_ord_connected_section {α : Type u_1} [linear_order α] (s : set α) :

(⇑order_dual.of_dual ⁻¹' s).ord_connected_section = ⇑order_dual.of_dual ⁻¹' s.ord_connected_section

theorem set.ord_connected_section_subset {α : Type u_1} [linear_order α] {s : set α} :

s.ord_connected_section ⊆ s

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 : set.uIcc x 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

s.ord_separating_set t = (⋃ (x : α) (H : x ∈ s), tᶜ.ord_connected_component x) ∩ ⋃ (x : α) (H : x ∈ t), sᶜ.ord_connected_component x

theorem set.ord_separating_set_comm {α : Type u_1} [linear_order α] (s t : set α) :

s.ord_separating_set t = t.ord_separating_set s

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

disjoint s (s.ord_separating_set t)

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

disjoint t (s.ord_separating_set t)

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

(⇑order_dual.of_dual ⁻¹' s).ord_separating_set (⇑order_dual.of_dual ⁻¹' t) = ⇑order_dual.of_dual ⁻¹' s.ord_separating_set t

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

s.ord_t5_nhd t = ⋃ (x : α) (H : x ∈ s), (tᶜ ∩ (s.ord_separating_set t).ord_connected_sectionᶜ).ord_connected_component x

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

disjoint (s.ord_t5_nhd t) (t.ord_t5_nhd s)