# Documentation

Mathlib.Topology.Inseparable

# Inseparable points in a topological space #

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;

• InseparableSetoid X: same relation, as a setoid;

• SeparationQuotient X: the quotient of X by its InseparableSetoid.

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 : X) (y : X) :

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.

Instances For

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.

Instances For
theorem specializes_TFAE {X : Type u_1} [] (x : X) (y : X) :
List.TFAE [x y, pure x nhds y, ∀ (s : Set X), y sx s, ∀ (s : Set X), x sy s, y closure {x}, closure {y} closure {x}, ClusterPt y (pure x)]

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 : X} {y : X} :
x y nhds x nhds y
theorem specializes_iff_pure {X : Type u_1} [] {x : X} {y : X} :
x y pure x nhds y
theorem Specializes.nhds_le_nhds {X : Type u_1} [] {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} [] {x : X} {y : X} :
x ypure x nhds y

Alias of the forward direction of specializes_iff_pure.

theorem ker_nhds_eq_specializes {X : Type u_1} [] {x : X} :
Filter.ker (nhds x) = {y | y x}
theorem specializes_iff_forall_open {X : Type u_1} [] {x : X} {y : X} :
x y ∀ (s : Set X), y sx s
theorem Specializes.mem_open {X : Type u_1} [] {x : X} {y : X} {s : Set X} (h : x y) (hs : ) (hy : y s) :
x s
theorem IsOpen.not_specializes {X : Type u_1} [] {x : X} {y : X} {s : Set X} (hs : ) (hx : ¬x s) (hy : y s) :
¬x y
theorem specializes_iff_forall_closed {X : Type u_1} [] {x : X} {y : X} :
x y ∀ (s : Set X), x sy s
theorem Specializes.mem_closed {X : Type u_1} [] {x : X} {y : X} {s : Set X} (h : x y) (hs : ) (hx : x s) :
y s
theorem IsClosed.not_specializes {X : Type u_1} [] {x : X} {y : X} {s : Set X} (hs : ) (hx : x s) (hy : ¬y s) :
¬x y
theorem specializes_iff_mem_closure {X : Type u_1} [] {x : X} {y : X} :
x y y closure {x}
theorem Specializes.mem_closure {X : Type u_1} [] {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} [] {x : X} {y : X} :
x y closure {y} closure {x}
theorem Specializes.closure_subset {X : Type u_1} [] {x : X} {y : X} :
x yclosure {y} closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

theorem specializes_iff_clusterPt {X : Type u_1} [] {x : X} {y : X} :
x y ClusterPt y (pure x)
theorem Filter.HasBasis.specializes_iff {X : Type u_1} [] {x : X} {y : X} {ι : Sort u_7} {p : ιProp} {s : ιSet X} (h : Filter.HasBasis (nhds y) p s) :
x y ∀ (i : ι), p ix s i
theorem specializes_rfl {X : Type u_1} [] {x : X} :
x x
theorem specializes_refl {X : Type u_1} [] (x : X) :
x x
theorem Specializes.trans {X : Type u_1} [] {x : X} {y : X} {z : X} :
x yy zx z
theorem specializes_of_eq {X : Type u_1} [] {x : X} {y : X} (e : x = y) :
x y
theorem specializes_of_nhdsWithin {X : Type u_1} [] {x : X} {y : X} {s : Set X} (h₁ : ) (h₂ : x s) :
x y
theorem Specializes.map_of_continuousAt {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (h : x y) (hy : ) :
f x f y
theorem Specializes.map {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (h : x y) (hf : ) :
f x f y
theorem Inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (hf : ) :
f x f y x y
theorem subtype_specializes_iff {X : Type u_1} [] {p : XProp} (x : ) (y : ) :
x y x y
@[simp]
theorem specializes_prod {X : Type u_1} {Y : Type u_2} [] [] {x₁ : X} {x₂ : X} {y₁ : 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₂ : X} {y₁ : Y} {y₂ : Y} (hx : x₁ x₂) (hy : y₁ y₂) :
(x₁, y₁) (x₂, y₂)
@[simp]
theorem specializes_pi {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : (i : ι) → π i} {g : (i : ι) → π i} :
f g ∀ (i : ι), f i g i
theorem not_specializes_iff_exists_open {X : Type u_1} [] {x : X} {y : X} :
¬x y S, y S ¬x S
theorem not_specializes_iff_exists_closed {X : Type u_1} [] {x : X} {y : X} :
¬x y S, x S ¬y S
def specializationPreorder (X : Type u_1) [] :

Specialization forms a preorder on the topological space.

Instances For
theorem Continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :

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 : X) (y : X) :

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.
Instances For
theorem inseparable_def {X : Type u_1} [] {x : X} {y : X} :
nhds x = nhds y
theorem inseparable_iff_specializes_and {X : Type u_1} [] {x : X} {y : X} :
x y y x
theorem Inseparable.specializes {X : Type u_1} [] {x : X} {y : X} (h : ) :
x y
theorem Inseparable.specializes' {X : Type u_1} [] {x : X} {y : X} (h : ) :
y x
theorem Specializes.antisymm {X : Type u_1} [] {x : X} {y : X} (h₁ : x y) (h₂ : y x) :
theorem inseparable_iff_forall_open {X : Type u_1} [] {x : X} {y : X} :
∀ (s : Set X), → (x s y s)
theorem not_inseparable_iff_exists_open {X : Type u_1} [] {x : X} {y : X} :
¬ s, Xor' (x s) (y s)
theorem inseparable_iff_forall_closed {X : Type u_1} [] {x : X} {y : X} :
∀ (s : Set X), → (x s y s)
theorem inseparable_iff_mem_closure {X : Type u_1} [] {x : X} {y : X} :
x closure {y} y closure {x}
theorem inseparable_iff_closure_eq {X : Type u_1} [] {x : X} {y : X} :
closure {x} = closure {y}
theorem inseparable_of_nhdsWithin_eq {X : Type u_1} [] {x : X} {y : X} {s : Set X} (hx : x s) (hy : y s) (h : = ) :
theorem Inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (hf : ) :
Inseparable (f x) (f y)
theorem subtype_inseparable_iff {X : Type u_1} [] {p : XProp} (x : ) (y : ) :
Inseparable x y
@[simp]
theorem inseparable_prod {X : Type u_1} {Y : Type u_2} [] [] {x₁ : X} {x₂ : X} {y₁ : Y} {y₂ : Y} :
Inseparable (x₁, y₁) (x₂, y₂) Inseparable x₁ x₂ Inseparable y₁ y₂
theorem Inseparable.prod {X : Type u_1} {Y : Type u_2} [] [] {x₁ : X} {x₂ : X} {y₁ : Y} {y₂ : Y} (hx : Inseparable x₁ x₂) (hy : Inseparable y₁ y₂) :
Inseparable (x₁, y₁) (x₂, y₂)
@[simp]
theorem inseparable_pi {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : (i : ι) → π i} {g : (i : ι) → π i} :
∀ (i : ι), Inseparable (f i) (g i)
theorem Inseparable.refl {X : Type u_1} [] (x : X) :
theorem Inseparable.rfl {X : Type u_1} [] {x : X} :
theorem Inseparable.of_eq {X : Type u_1} [] {x : X} {y : X} (e : x = y) :
theorem Inseparable.symm {X : Type u_1} [] {x : X} {y : X} (h : ) :
theorem Inseparable.trans {X : Type u_1} [] {x : X} {y : X} {z : X} (h₁ : ) (h₂ : ) :
theorem Inseparable.nhds_eq {X : Type u_1} [] {x : X} {y : X} (h : ) :
nhds x = nhds y
theorem Inseparable.mem_open_iff {X : Type u_1} [] {x : X} {y : X} {s : Set X} (h : ) (hs : ) :
x s y s
theorem Inseparable.mem_closed_iff {X : Type u_1} [] {x : X} {y : X} {s : Set X} (h : ) (hs : ) :
x s y s
theorem Inseparable.map_of_continuousAt {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (h : ) (hx : ) (hy : ) :
Inseparable (f x) (f y)
theorem Inseparable.map {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : X} {f : XY} (h : ) (hf : ) :
Inseparable (f x) (f y)
theorem IsClosed.not_inseparable {X : Type u_1} [] {x : X} {y : X} {s : Set X} (hs : ) (hx : x s) (hy : ¬y s) :
theorem IsOpen.not_inseparable {X : Type u_1} [] {x : X} {y : X} {s : Set X} (hs : ) (hx : x s) (hy : ¬y s) :

### Separation quotient #

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

def inseparableSetoid (X : Type u_1) [] :

A setoid version of Inseparable, used to define the SeparationQuotient.

Instances For
def SeparationQuotient (X : Type u_1) [] :
Type u_1

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

Instances For
def SeparationQuotient.mk {X : Type u_1} [] :

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

Instances For
theorem SeparationQuotient.quotientMap_mk {X : Type u_1} [] :
QuotientMap SeparationQuotient.mk
theorem SeparationQuotient.continuous_mk {X : Type u_1} [] :
Continuous SeparationQuotient.mk
@[simp]
theorem SeparationQuotient.mk_eq_mk {X : Type u_1} [] {x : X} {y : X} :
theorem SeparationQuotient.surjective_mk {X : Type u_1} [] :
Function.Surjective SeparationQuotient.mk
@[simp]
theorem SeparationQuotient.range_mk {X : Type u_1} [] :
Set.range SeparationQuotient.mk = Set.univ
theorem SeparationQuotient.preimage_image_mk_open {X : Type u_1} [] {s : Set X} (hs : ) :
SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s
theorem SeparationQuotient.isOpenMap_mk {X : Type u_1} [] :
IsOpenMap SeparationQuotient.mk
theorem SeparationQuotient.preimage_image_mk_closed {X : Type u_1} [] {s : Set X} (hs : ) :
SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s
theorem SeparationQuotient.inducing_mk {X : Type u_1} [] :
Inducing SeparationQuotient.mk
theorem SeparationQuotient.isClosedMap_mk {X : Type u_1} [] :
IsClosedMap SeparationQuotient.mk
@[simp]
theorem SeparationQuotient.comap_mk_nhds_mk {X : Type u_1} [] {x : X} :
Filter.comap SeparationQuotient.mk () = nhds x
@[simp]
theorem SeparationQuotient.comap_mk_nhdsSet_image {X : Type u_1} [] {s : Set X} :
Filter.comap SeparationQuotient.mk (nhdsSet (SeparationQuotient.mk '' s)) =
theorem SeparationQuotient.map_mk_nhds {X : Type u_1} [] {x : X} :
Filter.map SeparationQuotient.mk (nhds x) =
theorem SeparationQuotient.map_mk_nhdsSet {X : Type u_1} [] {s : Set X} :
Filter.map SeparationQuotient.mk () = nhdsSet (SeparationQuotient.mk '' s)
theorem SeparationQuotient.comap_mk_nhdsSet {X : Type u_1} [] {t : } :
Filter.comap SeparationQuotient.mk () = nhdsSet (SeparationQuotient.mk ⁻¹' t)
theorem SeparationQuotient.preimage_mk_closure {X : Type u_1} [] {t : } :
SeparationQuotient.mk ⁻¹' = closure (SeparationQuotient.mk ⁻¹' t)
theorem SeparationQuotient.preimage_mk_interior {X : Type u_1} [] {t : } :
SeparationQuotient.mk ⁻¹' = interior (SeparationQuotient.mk ⁻¹' t)
theorem SeparationQuotient.preimage_mk_frontier {X : Type u_1} [] {t : } :
SeparationQuotient.mk ⁻¹' = frontier (SeparationQuotient.mk ⁻¹' t)
theorem SeparationQuotient.image_mk_closure {X : Type u_1} [] {s : Set X} :
SeparationQuotient.mk '' = closure (SeparationQuotient.mk '' s)
theorem SeparationQuotient.map_prod_map_mk_nhds {X : Type u_1} {Y : Type u_2} [] [] (x : X) (y : Y) :
Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (nhds (x, y)) =
theorem SeparationQuotient.map_mk_nhdsWithin_preimage {X : Type u_1} [] (s : ) (x : X) :
Filter.map SeparationQuotient.mk (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) =
def SeparationQuotient.lift {X : Type u_1} {α : Type u_4} [] (f : Xα) (hf : ∀ (x y : X), f x = f y) :

Lift a map f : X → α such that Inseparable x y → f x = f y to a map SeparationQuotient X → α.

Instances For
@[simp]
theorem SeparationQuotient.lift_mk {X : Type u_1} {α : Type u_4} [] {f : Xα} (hf : ∀ (x y : X), f x = f y) (x : X) :
= f x
@[simp]
theorem SeparationQuotient.lift_comp_mk {X : Type u_1} {α : Type u_4} [] {f : Xα} (hf : ∀ (x y : X), f x = f y) :
SeparationQuotient.mk = f
@[simp]
theorem SeparationQuotient.tendsto_lift_nhds_mk {X : Type u_1} {α : Type u_4} [] {f : Xα} {hf : ∀ (x y : X), f x = f y} {x : X} {l : } :
@[simp]
theorem SeparationQuotient.tendsto_lift_nhdsWithin_mk {X : Type u_1} {α : Type u_4} [] {f : Xα} {hf : ∀ (x y : X), f x = f y} {x : X} {s : } {l : } :
Filter.Tendsto () () l Filter.Tendsto f (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) l
@[simp]
theorem SeparationQuotient.continuousAt_lift {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {hf : ∀ (x y : X), f x = f y} {x : X} :
@[simp]
theorem SeparationQuotient.continuousWithinAt_lift {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {hf : ∀ (x y : X), f x = f y} {s : } {x : X} :
ContinuousWithinAt f (SeparationQuotient.mk ⁻¹' s) x
@[simp]
theorem SeparationQuotient.continuousOn_lift {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {hf : ∀ (x y : X), f x = f y} {s : } :
ContinuousOn f (SeparationQuotient.mk ⁻¹' s)
@[simp]
theorem SeparationQuotient.continuous_lift {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {hf : ∀ (x y : X), f x = f y} :
def SeparationQuotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [] [] (f : XYα) (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), 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 SeparationQuotient X → SeparationQuotient Y → α.

Instances For
@[simp]
theorem SeparationQuotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} [] [] {f : XYα} (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d) (x : X) (y : Y) :
= f x y
@[simp]
theorem SeparationQuotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} [] [] {f : XYα} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} {x : X} {y : Y} {l : } :
Filter.Tendsto () () l Filter.Tendsto () (nhds (x, y)) l
@[simp]
theorem SeparationQuotient.tendsto_lift₂_nhdsWithin {X : Type u_1} {Y : Type u_2} {α : Type u_4} [] [] {f : XYα} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} {x : X} {y : Y} {s : } {l : } :
Filter.Tendsto () () l Filter.Tendsto () (nhdsWithin (x, y) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)) l
@[simp]
theorem SeparationQuotient.continuousAt_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} {x : X} {y : Y} :
ContinuousAt () (x, y)
@[simp]
theorem SeparationQuotient.continuousWithinAt_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} {s : } {x : X} {y : Y} :
ContinuousWithinAt () (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s) (x, y)
@[simp]
theorem SeparationQuotient.continuousOn_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} {s : } :
ContinuousOn () (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)
@[simp]
theorem SeparationQuotient.continuous_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), f a b = f c d} :