# mathlib3documentation

topology.inseparable

# Inseparable points in a topological space #

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

In this file we define

• specializes (notation: x ⤳ y) : a relation saying that 𝓝 x ≤ 𝓝 y;

• inseparable: a relation saying that two points in a topological space have the same neighbourhoods; equivalently, they can't be separated by an open set;

• inseparable_setoid X: same relation, as a setoid;

• separation_quotient X: the quotient of X by its inseparable_setoid.

We also prove various basic properties of the relation inseparable.

## Notations #

• x ⤳ y: notation for specializes x y;
• x ~ y is used as a local notation for inseparable x y;
• 𝓝 x is the neighbourhoods filter nhds x of a point x, defined elsewhere.

## Tags #

topological space, separation setoid

### specializes relation #

def specializes {X : Type u_1} (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} (x y : X) :
[x y, , (s : set X), y s x s, (s : set X), x s y s, y closure {x}, closure {y} closure {x}, (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} {x y : X} :
x y nhds x nhds y
theorem specializes_iff_pure {X : Type u_1} {x y : X} :
x y
theorem specializes.nhds_le_nhds {X : Type u_1} {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} {x y : X} :
x y

Alias of the forward direction of specializes_iff_pure.

theorem specializes_iff_forall_open {X : Type u_1} {x y : X} :
x y (s : set X), y s x s
theorem specializes.mem_open {X : Type u_1} {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} {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} {x y : X} :
x y (s : set X), x s y s
theorem specializes.mem_closed {X : Type u_1} {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} {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} {x y : X} :
x y y closure {x}
theorem specializes.mem_closure {X : Type u_1} {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} {x y : X} :
x y closure {y} closure {x}
theorem specializes.closure_subset {X : Type u_1} {x y : X} :
x y closure {y} closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

theorem filter.has_basis.specializes_iff {X : Type u_1} {x y : X} {ι : Sort u_2} {p : ι Prop} {s : ι set X} (h : (nhds y).has_basis p s) :
x y (i : ι), p i x s i
theorem specializes_rfl {X : Type u_1} {x : X} :
x x
@[refl]
theorem specializes_refl {X : Type u_1} (x : X) :
x x
@[trans]
theorem specializes.trans {X : Type u_1} {x y z : X} :
x y y z x z
theorem specializes_of_eq {X : Type u_1} {x y : X} (e : x = y) :
x y
theorem specializes_of_nhds_within {X : Type u_1} {x y : X} {s : set X} (h₁ : s s) (h₂ : x s) :
x y
theorem specializes.map_of_continuous_at {X : Type u_1} {Y : Type u_2} {x y : X} {f : X Y} (h : x y) (hy : y) :
f x f y
theorem specializes.map {X : Type u_1} {Y : Type u_2} {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} {x y : X} {f : X Y} (hf : inducing f) :
f x f y x y
theorem subtype_specializes_iff {X : Type u_1} {p : X Prop} (x y : subtype p) :
x y x y
@[simp]
theorem specializes_prod {X : Type u_1} {Y : Type u_2} {x₁ x₂ : X} {y₁ y₂ : Y} :
(x₁, y₁) (x₂, y₂) x₁ x₂ y₁ y₂
theorem specializes.prod {X : Type u_1} {Y : Type u_2} {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ x₂) (hy : y₁ y₂) :
(x₁, y₁) (x₂, y₂)
@[simp]
theorem specializes_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
f g (i : ι), f i g i
theorem not_specializes_iff_exists_open {X : Type u_1} {x y : X} :
¬x y (S : set X), y S x S
theorem not_specializes_iff_exists_closed {X : Type u_1} {x y : X} :
¬x y (S : set X), x S y S
def specialization_preorder (X : Type u_1)  :

Specialization forms a preorder on the topological space.

Equations
theorem continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} {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} (x y : X) :
Prop

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

• 𝓝 x = 𝓝 y; we use this property as the definition;
• for any open set s, x ∈ s ↔ y ∈ s, see inseparable_iff_open;
• for any closed set s, x ∈ s ↔ y ∈ s, see inseparable_iff_closed;
• x ∈ closure {y} and y ∈ closure {x}, see inseparable_iff_mem_closure;
• closure {x} = closure {y}, see inseparable_iff_closure_eq.
Equations
theorem inseparable_def {X : Type u_1} {x y : X} :
y nhds x = nhds y
theorem inseparable_iff_specializes_and {X : Type u_1} {x y : X} :
y x y y x
theorem inseparable.specializes {X : Type u_1} {x y : X} (h : y) :
x y
theorem inseparable.specializes' {X : Type u_1} {x y : X} (h : y) :
y x
theorem specializes.antisymm {X : Type u_1} {x y : X} (h₁ : x y) (h₂ : y x) :
y
theorem inseparable_iff_forall_open {X : Type u_1} {x y : X} :
y (s : set X), (x s y s)
theorem not_inseparable_iff_exists_open {X : Type u_1} {x y : X} :
¬ y (s : set X), xor (x s) (y s)
theorem inseparable_iff_forall_closed {X : Type u_1} {x y : X} :
y (s : set X), (x s y s)
theorem inseparable_iff_mem_closure {X : Type u_1} {x y : X} :
y x closure {y} y closure {x}
theorem inseparable_iff_closure_eq {X : Type u_1} {x y : X} :
y closure {x} = closure {y}
theorem inseparable_of_nhds_within_eq {X : Type u_1} {x y : X} {s : set X} (hx : x s) (hy : y s) (h : s = s) :
y
theorem inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} {x y : X} {f : X Y} (hf : inducing f) :
inseparable (f x) (f y) y
theorem subtype_inseparable_iff {X : Type u_1} {p : X Prop} (x y : subtype p) :
y
@[simp]
theorem inseparable_prod {X : Type u_1} {Y : Type u_2} {x₁ x₂ : X} {y₁ y₂ : Y} :
inseparable (x₁, y₁) (x₂, y₂) x₂ y₂
theorem inseparable.prod {X : Type u_1} {Y : Type u_2} {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₂) (hy : y₂) :
inseparable (x₁, y₁) (x₂, y₂)
@[simp]
theorem inseparable_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
g (i : ι), inseparable (f i) (g i)
@[refl]
theorem inseparable.refl {X : Type u_1} (x : X) :
x
theorem inseparable.rfl {X : Type u_1} {x : X} :
x
theorem inseparable.of_eq {X : Type u_1} {x y : X} (e : x = y) :
y
@[symm]
theorem inseparable.symm {X : Type u_1} {x y : X} (h : y) :
x
@[trans]
theorem inseparable.trans {X : Type u_1} {x y z : X} (h₁ : y) (h₂ : z) :
z
theorem inseparable.nhds_eq {X : Type u_1} {x y : X} (h : y) :
nhds x = nhds y
theorem inseparable.mem_open_iff {X : Type u_1} {x y : X} {s : set X} (h : y) (hs : is_open s) :
x s y s
theorem inseparable.mem_closed_iff {X : Type u_1} {x y : X} {s : set X} (h : y) (hs : is_closed s) :
x s y s
theorem inseparable.map_of_continuous_at {X : Type u_1} {Y : Type u_2} {x y : X} {f : X Y} (h : y) (hx : x) (hy : y) :
inseparable (f x) (f y)
theorem inseparable.map {X : Type u_1} {Y : Type u_2} {x y : X} {f : X Y} (h : y) (hf : continuous f) :
inseparable (f x) (f y)
theorem is_closed.not_inseparable {X : Type u_1} {x y : X} {s : set X} (hs : is_closed s) (hx : x s) (hy : y s) :
¬ y
theorem is_open.not_inseparable {X : Type u_1} {x y : X} {s : set X} (hs : is_open s) (hx : x s) (hy : y s) :
¬ y

### Separation quotient #

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

def inseparable_setoid (X : Type u_1)  :

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

Equations
@[protected, instance]
def separation_quotient (X : Type u_1)  :
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}  :

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

Equations
@[simp]
theorem separation_quotient.mk_eq_mk {X : Type u_1} {x y : X} :
@[simp]
theorem separation_quotient.range_mk {X : Type u_1}  :
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
theorem separation_quotient.preimage_image_mk_open {X : Type u_1} {s : set X} (hs : is_open s) :
theorem separation_quotient.preimage_image_mk_closed {X : Type u_1} {s : set X} (hs : is_closed s) :
@[simp]
theorem separation_quotient.comap_mk_nhds_mk {X : Type u_1} {x : X} :
@[simp]
theorem separation_quotient.map_mk_nhds {X : Type u_1} {x : X} :
theorem separation_quotient.map_mk_nhds_set {X : Type u_1} {s : set X} :
theorem separation_quotient.image_mk_closure {X : Type u_1} {s : set X} :
theorem separation_quotient.map_prod_map_mk_nhds {X : Type u_1} {Y : Type u_2} (x : X) (y : Y) :
theorem separation_quotient.map_mk_nhds_within_preimage {X : Type u_1} (s : set ) (x : X) :
def separation_quotient.lift {X : Type u_1} {α : Type u_4} (f : X α) (hf : (x y : X), y f x = f y) :

Lift a map f : X → α such that inseparable x y → f x = f y to a map separation_quotient X → α.

Equations
• = λ (x : , hf
@[simp]
theorem separation_quotient.lift_mk {X : Type u_1} {α : Type u_4} {f : X α} (hf : (x y : X), y f x = f y) (x : X) :
= f x
@[simp]
theorem separation_quotient.lift_comp_mk {X : Type u_1} {α : Type u_4} {f : X α} (hf : (x y : X), y f x = f y) :
@[simp]
theorem separation_quotient.tendsto_lift_nhds_mk {X : Type u_1} {α : Type u_4} {f : X α} {hf : (x y : X), y f x = f y} {x : X} {l : filter α} :
l (nhds x) l
@[simp]
theorem separation_quotient.tendsto_lift_nhds_within_mk {X : Type u_1} {α : Type u_4} {f : X α} {hf : (x y : X), y f x = f y} {x : X} {s : set } {l : filter α} :
l l
@[simp]
theorem separation_quotient.continuous_at_lift {X : Type u_1} {Y : Type u_2} {f : X Y} {hf : (x y : X), y f x = f y} {x : X} :
@[simp]
theorem separation_quotient.continuous_within_at_lift {X : Type u_1} {Y : Type u_2} {f : X Y} {hf : (x y : X), y f x = f y} {s : set } {x : X} :
@[simp]
theorem separation_quotient.continuous_on_lift {X : Type u_1} {Y : Type u_2} {f : X Y} {hf : (x y : X), y f x = f y} {s : set } :
@[simp]
theorem separation_quotient.continuous_lift {X : Type u_1} {Y : Type u_2} {f : X Y} {hf : (x y : X), y f x = f y} :
def separation_quotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} (f : X Y α) (hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d) :

Lift a map f : X → Y → α such that inseparable a b → inseparable c d → f a c = f b d to a map separation_quotient X → separation_quotient Y → α.

Equations
• = λ (x : (y : , f hf
@[simp]
theorem separation_quotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} {f : X Y α} (hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d) (x : X) (y : Y) :
= f x y
@[simp]
theorem separation_quotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} {f : X Y α} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} {x : X} {y : Y} {l : filter α} :
(nhds (x, y)) l
@[simp]
theorem separation_quotient.tendsto_lift₂_nhds_within {X : Type u_1} {Y : Type u_2} {α : Type u_4} {f : X Y α} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} {x : X} {y : Y} {s : set } {l : filter α} :
l
@[simp]
theorem separation_quotient.continuous_at_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} {x : X} {y : Y} :
(x, y)
@[simp]
theorem separation_quotient.continuous_within_at_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} {s : set } {x : X} {y : Y} :
@[simp]
theorem separation_quotient.continuous_on_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} {s : set } :
@[simp]
theorem separation_quotient.continuous_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), c d f a b = f c d} :