mathlib documentation

topology.inseparable

Inseparable points in a topological space #

In this file we define

We also prove various basic properties of the relation inseparable.

Notations #

Tags #

topological space, separation setoid

specializes relation #

def specializes {X : Type u_1} [topological_space X] (x y : X) :
Prop

x specializes to y (notation: x ⤳ y) if either of the following equivalent properties hold:

  • 𝓝 x ≤ 𝓝 y; this property is used as the definition;
  • pure x ≤ 𝓝 y; in other words, any neighbourhood of y contains x;
  • y ∈ closure {x};
  • closure {y} ⊆ closure {x};
  • for any closed set s we have x ∈ s → y ∈ s;
  • for any open set s we have y ∈ s → x ∈ s;
  • y is a cluster point of the filter pure x = 𝓟 {x}.

This relation defines a preorder on X. If X is a T₀ space, then this preorder is a partial order. If X is a T₁ space, then this partial order is trivial : x ⤳ y ↔ x = y.

Equations
theorem specializes_tfae {X : Type u_1} [topological_space X] (x y : X) :
[x ⤳ y, has_pure.pure x ≤ nhds y, ∀ (s : set X), is_open s → y ∈ s → x ∈ s, ∀ (s : set X), is_closed s → x ∈ s → y ∈ s, y ∈ closure {x}, closure {y} ⊆ closure {x}, cluster_pt y (has_pure.pure x)].tfae

A collection of equivalent definitions of x ⤳ y. The public API is given by iff lemmas below.

theorem specializes_iff_nhds {X : Type u_1} [topological_space X] {x y : X} :
theorem specializes_iff_pure {X : Type u_1} [topological_space X] {x y : X} :
theorem specializes.nhds_le_nhds {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → nhds x ≤ nhds y

Alias of the forward direction of specializes_iff_nhds.

theorem specializes.pure_le_nhds {X : Type u_1} [topological_space X] {x y : X} :

Alias of the forward direction of specializes_iff_pure.

theorem specializes_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ ∀ (s : set X), is_open s → y ∈ s → x ∈ s
theorem specializes.mem_open {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x ⤳ y) (hs : is_open s) (hy : y ∈ s) :
x ∈ s
theorem is_open.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x ∉ s) (hy : y ∈ s) :
theorem specializes_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y ↔ ∀ (s : set X), is_closed s → x ∈ s → y ∈ s
theorem specializes.mem_closed {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x ⤳ y) (hs : is_closed s) (hx : x ∈ s) :
y ∈ s
theorem is_closed.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) :
theorem specializes_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
theorem specializes.mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → y ∈ closure {x}

Alias of the forward direction of specializes_iff_mem_closure.

theorem specializes_iff_closure_subset {X : Type u_1} [topological_space X] {x y : X} :
theorem specializes.closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x ⤳ y → closure {y} ⊆ closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

theorem specializes_rfl {X : Type u_1} [topological_space X] {x : X} :
x ⤳ x
@[refl]
theorem specializes_refl {X : Type u_1} [topological_space X] (x : X) :
x ⤳ x
@[trans]
theorem specializes.trans {X : Type u_1} [topological_space X] {x y z : X} :
x ⤳ y → y ⤳ z → x ⤳ z
theorem specializes_of_nhds_within {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h₁ : nhds_within x s ≤ nhds_within y s) (h₂ : x ∈ s) :
x ⤳ y
theorem specializes.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hy : continuous_at f y) :
f x ⤳ f y
theorem specializes.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hf : continuous f) :
f x ⤳ f y
theorem inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (hf : inducing f) :
f x ⤳ f y ↔ x ⤳ y
theorem subtype_specializes_iff {X : Type u_1} [topological_space X] {p : X → Prop} (x y : subtype p) :
def specialization_preorder (X : Type u_1) [topological_space X] :

Specialization forms a preorder on the topological space.

Equations
theorem continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X → Y} (hf : continuous f) :

A continuous function is monotone with respect to the specialization preorders on the domain and the codomain.

inseparable relation #

def inseparable {X : Type u_1} [topological_space X] (x y : X) :
Prop

Two points x and y in a topological space are inseparable if any of the following equivalent properties hold:

Equations
theorem inseparable_def {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_iff_specializes_and {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable.specializes {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
x ⤳ y
theorem inseparable.specializes' {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
y ⤳ x
theorem specializes.antisymm {X : Type u_1} [topological_space X] {x y : X} (h₁ : x ⤳ y) (h₂ : y ⤳ x) :
theorem inseparable_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ ∀ (s : set X), is_open s → (x ∈ s ↔ y ∈ s)
theorem not_inseparable_iff_exists_open {X : Type u_1} [topological_space X] {x y : X} :
¬inseparable x y ↔ ∃ (s : set X), is_open s ∧ xor (x ∈ s) (y ∈ s)
theorem inseparable_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y ↔ ∀ (s : set X), is_closed s → (x ∈ s ↔ y ∈ s)
theorem inseparable_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_iff_closure_eq {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_of_nhds_within_eq {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hx : x ∈ s) (hy : y ∈ s) (h : nhds_within x s = nhds_within y s) :
theorem inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (hf : inducing f) :
theorem subtype_inseparable_iff {X : Type u_1} [topological_space X] {p : X → Prop} (x y : subtype p) :
@[refl]
theorem inseparable.refl {X : Type u_1} [topological_space X] (x : X) :
theorem inseparable.rfl {X : Type u_1} [topological_space X] {x : X} :
@[symm]
theorem inseparable.symm {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
@[trans]
theorem inseparable.trans {X : Type u_1} [topological_space X] {x y z : X} (h₁ : inseparable x y) (h₂ : inseparable y z) :
theorem inseparable.nhds_eq {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
nhds x = nhds y
theorem inseparable.mem_open_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_open s) :
theorem inseparable.mem_closed_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_closed s) :
theorem inseparable.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : inseparable x y) (hx : continuous_at f x) (hy : continuous_at f y) :
inseparable (f x) (f y)
theorem inseparable.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X → Y} (h : inseparable x y) (hf : continuous f) :
inseparable (f x) (f y)
theorem is_closed.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x ∈ s) (hy : y ∉ s) :
theorem is_open.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x ∈ s) (hy : y ∉ s) :

Separation quotient #

In this section we define the quotient of a topological space by the inseparable relation.

def inseparable_setoid (X : Type u_1) [topological_space X] :

A setoid version of inseparable, used to define the separation_quotient.

Equations
def separation_quotient (X : Type u_1) [topological_space X] :
Type u_1

The quotient of a topological space by its inseparable_setoid. This quotient is guaranteed to be a T₀ space.

Equations
Instances for separation_quotient
def separation_quotient.mk {X : Type u_1} [topological_space X] :

The natural map from a topological space to its separation quotient.

Equations
@[protected, instance]