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 sy sx s, ∀ (s : set X), is_closed sx sy 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} :
x y nhds x nhds y
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 ynhds 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 sy sx 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) :
¬x y
theorem specializes_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
x y ∀ (s : set X), is_closed sx sy 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) :
¬x y
theorem specializes_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x y y closure {x}
theorem specializes.mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x yy 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} :
x y closure {y} closure {x}
theorem specializes.closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x yclosure {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 yy zx 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) :
x y x y
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} :
inseparable x y x y 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) :
inseparable (f x) (f y) inseparable x y
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) :
x s y 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) :
x s y 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

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

Equations
@[protected, instance]