# mathlib3documentation

topology.separation

# Separation properties of topological spaces. #

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

This file defines the predicate `separated_nhds`, and common separation axioms (under the Kolmogorov classification).

## Main definitions #

• `separated_nhds`: Two `set`s are separated by neighbourhoods if they are contained in disjoint open sets.
• `t0_space`: A T₀/Kolmogorov space is a space where, for every two points `x ≠ y`, there is an open set that contains one, but not the other.
• `t1_space`: A T₁/Fréchet space is a space where every singleton set is closed. This is equivalent to, for every pair `x ≠ y`, there existing an open set containing `x` but not `y` (`t1_space_iff_exists_open` shows that these conditions are equivalent.)
• `t2_space`: A T₂/Hausdorff space is a space where, for every two points `x ≠ y`, there is two disjoint open sets, one containing `x`, and the other `y`.
• `t2_5_space`: A T₂.₅/Urysohn space is a space where, for every two points `x ≠ y`, there is two open sets, one containing `x`, and the other `y`, whose closures are disjoint.
• `t3_space`: A T₃ space, is one where given any closed `C` and `x ∉ C`, there is disjoint open sets containing `x` and `C` respectively. In `mathlib`, T₃ implies T₂.₅.
• `normal_space`: A T₄ space (sometimes referred to as normal, but authors vary on whether this includes T₂; `mathlib` does), is one where given two disjoint closed sets, we can find two open sets that separate them. In `mathlib`, T₄ implies T₃.
• `t5_space`: A T₅ space, also known as a completely normal Hausdorff space

## Main results #

### T₀ spaces #

• `is_closed.exists_closed_singleton` Given a closed set `S` in a compact T₀ space, there is some `x ∈ S` such that `{x}` is closed.
• `exists_open_singleton_of_open_finset` Given an open `finset` `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open.

### T₁ spaces #

• `is_closed_map_const`: The constant map is a closed map.
• `discrete_of_t1_of_finite`: A finite T₁ space must have the discrete topology.

### T₂ spaces #

• `t2_iff_nhds`: A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.
• `t2_iff_is_closed_diagonal`: A space is T₂ iff the `diagonal` of `α` (that is, the set of all points of the form `(a, a) : α × α`) is closed under the product topology.
• `finset_disjoint_finset_opens_of_t2`: Any two disjoint finsets are `separated_nhds`.
• Most topological constructions preserve Hausdorffness; these results are part of the typeclass inference system (e.g. `embedding.t2_space`)
• `set.eq_on.closure`: If two functions are equal on some set `s`, they are equal on its closure.
• `is_compact.is_closed`: All compact sets are closed.
• `locally_compact_of_compact_nhds`: If every point has a compact neighbourhood, then the space is locally compact.
• `totally_separated_space_of_t1_of_basis_clopen`: If `α` has a clopen basis, then it is a `totally_separated_space`.
• `loc_compact_t2_tot_disc_iff_tot_sep`: A locally compact T₂ space is totally disconnected iff it is totally separated.

If the space is also compact:

• `normal_of_compact_t2`: A compact T₂ space is a `normal_space`.
• `connected_components_eq_Inter_clopen`: The connected component of a point is the intersection of all its clopen neighbourhoods.
• `compact_t2_tot_disc_iff_tot_sep`: Being a `totally_disconnected_space` is equivalent to being a `totally_separated_space`.
• `connected_components.t2`: `connected_components α` is T₂ for `α` T₂ and compact.

### T₃ spaces #

• `disjoint_nested_nhds`: Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`, with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint.

## References #

https://en.wikipedia.org/wiki/Separation_axiom

def separated_nhds {α : Type u}  :
set α set α Prop

`separated_nhds` is a predicate on pairs of sub`set`s of a topological space. It holds if the two sub`set`s are contained in disjoint open sets.

Equations
theorem separated_nhds_iff_disjoint {α : Type u} {s t : set α} :
@[symm]
theorem separated_nhds.symm {α : Type u} {s t : set α} :
theorem separated_nhds.comm {α : Type u} (s t : set α) :
theorem separated_nhds.preimage {α : Type u} {β : Type v} {f : α β} {s t : set β} (h : t) (hf : continuous f) :
@[protected]
theorem separated_nhds.disjoint {α : Type u} {s t : set α} (h : t) :
t
theorem separated_nhds.disjoint_closure_left {α : Type u} {s t : set α} (h : t) :
theorem separated_nhds.disjoint_closure_right {α : Type u} {s t : set α} (h : t) :
(closure t)
theorem separated_nhds.empty_right {α : Type u} (s : set α) :
theorem separated_nhds.empty_left {α : Type u} (s : set α) :
theorem separated_nhds.mono {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h : t₂) (hs : s₁ s₂) (ht : t₁ t₂) :
t₁
theorem separated_nhds.union_left {α : Type u} {s t u : set α} :
theorem separated_nhds.union_right {α : Type u} {s t u : set α} (ht : t) (hu : u) :
(t u)
@[class]
structure t0_space (α : Type u)  :
Prop
• t0 : ⦃x y : α⦄, y x = y

A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair `x ≠ y`, there is an open set containing one but not the other. We formulate the definition in terms of the `inseparable` relation.

Instances of this typeclass
theorem t0_space_iff_inseparable (α : Type u)  :
(x y : α), y x = y
theorem t0_space_iff_not_inseparable (α : Type u)  :
(x y : α), x y ¬ y
theorem inseparable.eq {α : Type u} [t0_space α] {x y : α} (h : y) :
x = y
@[protected]
theorem inducing.injective {α : Type u} {β : Type v} [t0_space α] {f : α β} (hf : inducing f) :
@[protected]
theorem inducing.embedding {α : Type u} {β : Type v} [t0_space α] {f : α β} (hf : inducing f) :
theorem embedding_iff_inducing {α : Type u} {β : Type v} [t0_space α] {f : α β} :
theorem t0_space_iff_nhds_injective (α : Type u)  :
theorem nhds_injective {α : Type u} [t0_space α] :
theorem inseparable_iff_eq {α : Type u} [t0_space α] {x y : α} :
y x = y
@[simp]
theorem nhds_eq_nhds_iff {α : Type u} [t0_space α] {a b : α} :
nhds a = nhds b a = b
@[simp]
theorem inseparable_eq_eq {α : Type u} [t0_space α] :
theorem t0_space_iff_exists_is_open_xor_mem (α : Type u)  :
(x y : α), x y ( (U : set α), xor (x U) (y U))
theorem exists_is_open_xor_mem {α : Type u} [t0_space α] {x y : α} (h : x y) :
(U : set α), xor (x U) (y U)
def specialization_order (α : Type u_1) [t0_space α] :

Specialization forms a partial order on a t0 topological space.

Equations
@[protected, instance]
theorem minimal_nonempty_closed_subsingleton {α : Type u} [t0_space α] {s : set α} (hs : is_closed s) (hmin : (t : set α), t s t.nonempty t = s) :
theorem minimal_nonempty_closed_eq_singleton {α : Type u} [t0_space α] {s : set α} (hs : is_closed s) (hne : s.nonempty) (hmin : (t : set α), t s t.nonempty t = s) :
(x : α), s = {x}
theorem is_closed.exists_closed_singleton {α : Type u_1} [t0_space α] {S : set α} (hS : is_closed S) (hne : S.nonempty) :
(x : α), x S is_closed {x}

Given a closed set `S` in a compact T₀ space, there is some `x ∈ S` such that `{x}` is closed.

theorem minimal_nonempty_open_subsingleton {α : Type u} [t0_space α] {s : set α} (hs : is_open s) (hmin : (t : set α), t s t.nonempty t = s) :
theorem minimal_nonempty_open_eq_singleton {α : Type u} [t0_space α] {s : set α} (hs : is_open s) (hne : s.nonempty) (hmin : (t : set α), t s t.nonempty t = s) :
(x : α), s = {x}
theorem exists_open_singleton_of_open_finite {α : Type u} [t0_space α] {s : set α} (hfin : s.finite) (hne : s.nonempty) (ho : is_open s) :
(x : α) (H : x s), is_open {x}

Given an open finite set `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open.

theorem exists_open_singleton_of_fintype {α : Type u} [t0_space α] [finite α] [nonempty α] :
(x : α), is_open {x}
theorem t0_space_of_injective_of_continuous {α : Type u} {β : Type v} {f : α β} (hf : function.injective f) (hf' : continuous f) [t0_space β] :
@[protected]
theorem embedding.t0_space {α : Type u} {β : Type v} [t0_space β] {f : α β} (hf : embedding f) :
@[protected, instance]
def subtype.t0_space {α : Type u} [t0_space α] {p : α Prop} :
theorem t0_space_iff_or_not_mem_closure (α : Type u)  :
(a b : α), a b a closure {b} b closure {a}
@[protected, instance]
def prod.t0_space {α : Type u} {β : Type v} [t0_space α] [t0_space β] :
t0_space × β)
@[protected, instance]
def pi.t0_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), t0_space (π i)] :
t0_space (Π (i : ι), π i)
theorem t0_space.of_cover {α : Type u} (h : (x y : α), y ( (s : set α), x s y s ) :
theorem t0_space.of_open_cover {α : Type u} (h : (x : α), (s : set α), x s ) :
@[class]
structure t1_space (α : Type u)  :
Prop

A T₁ space, also known as a Fréchet space, is a topological space where every singleton set is closed. Equivalently, for every pair `x ≠ y`, there is an open set containing `x` and not `y`.

Instances of this typeclass
theorem is_closed_singleton {α : Type u} [t1_space α] {x : α} :
theorem is_open_compl_singleton {α : Type u} [t1_space α] {x : α} :
theorem is_open_ne {α : Type u} [t1_space α] {x : α} :
is_open {y : α | y x}
theorem continuous.is_open_support {α : Type u} {β : Type v} [t1_space α] [has_zero α] {f : β α} (hf : continuous f) :
theorem continuous.is_open_mul_support {α : Type u} {β : Type v} [t1_space α] [has_one α] {f : β α} (hf : continuous f) :
theorem ne.nhds_within_compl_singleton {α : Type u} [t1_space α] {x y : α} (h : x y) :
{y} = nhds x
theorem ne.nhds_within_diff_singleton {α : Type u} [t1_space α] {x y : α} (h : x y) (s : set α) :
(s \ {y}) = s
theorem is_open_set_of_eventually_nhds_within {α : Type u} [t1_space α] {p : α Prop} :
is_open {x : α | ∀ᶠ (y : α) in {x}, p y}
@[protected]
theorem set.finite.is_closed {α : Type u} [t1_space α] {s : set α} (hs : s.finite) :
theorem topological_space.is_topological_basis.exists_mem_of_ne {α : Type u} [t1_space α] {b : set (set α)} {x y : α} (h : x y) :
(a : set α) (H : a b), x a y a

In a `t1_space`, relatively compact sets form a bornology. Its cobounded filter is `filter.coclosed_compact`. See also `bornology.in_compact` the bornology of sets contained in a compact set.

Equations
@[protected]
theorem finset.is_closed {α : Type u} [t1_space α] (s : finset α) :
theorem t1_space_tfae (α : Type u)  :
[, (x : α), is_closed {x}, (x : α), is_open {x}, , ⦃x y : α⦄, x y {y} nhds x, ⦃x y : α⦄, x y ( (s : set α) (H : s nhds x), y s), ⦃x y : α⦄, x y ( (U : set α) (hU : is_open U), x U y U), ⦃x y : α⦄, x y disjoint (nhds x) , ⦃x y : α⦄, x y (nhds y), ⦃x y : α⦄, x y x = y].tfae
theorem t1_space_iff_exists_open {α : Type u}  :
(x y : α), x y ( (U : set α) (hU : is_open U), x U y U)
theorem t1_space_iff_disjoint_pure_nhds {α : Type u}  :
⦃x y : α⦄, x y (nhds y)
theorem t1_space_iff_disjoint_nhds_pure {α : Type u}  :
⦃x y : α⦄, x y disjoint (nhds x)
theorem t1_space_iff_specializes_imp_eq {α : Type u}  :
⦃x y : α⦄, x y x = y
theorem disjoint_pure_nhds {α : Type u} [t1_space α] {x y : α} (h : x y) :
(nhds y)
theorem disjoint_nhds_pure {α : Type u} [t1_space α] {x y : α} (h : x y) :
theorem specializes.eq {α : Type u} [t1_space α] {x y : α} (h : x y) :
x = y
theorem specializes_iff_eq {α : Type u} [t1_space α] {x y : α} :
x y x = y
@[simp]
theorem specializes_eq_eq {α : Type u} [t1_space α] :
@[simp]
theorem pure_le_nhds_iff {α : Type u} [t1_space α] {a b : α} :
a = b
@[simp]
theorem nhds_le_nhds_iff {α : Type u} [t1_space α] {a b : α} :
nhds a nhds b a = b
@[protected, instance]
def cofinite_topology.t1_space {α : Type u_1} :
theorem t1_space_antitone {α : Type u_1} :
theorem continuous_within_at_update_of_ne {α : Type u} {β : Type v} [t1_space α] [decidable_eq α] {f : α β} {s : set α} {x y : α} {z : β} (hne : y x) :
s y y
theorem continuous_at_update_of_ne {α : Type u} {β : Type v} [t1_space α] [decidable_eq α] {f : α β} {x y : α} {z : β} (hne : y x) :
theorem continuous_on_update_iff {α : Type u} {β : Type v} [t1_space α] [decidable_eq α] {f : α β} {s : set α} {x : α} {y : β} :
continuous_on x y) s (s \ {x}) (x s (s \ {x})) (nhds y))
theorem t1_space_of_injective_of_continuous {α : Type u} {β : Type v} {f : α β} (hf : function.injective f) (hf' : continuous f) [t1_space β] :
@[protected]
theorem embedding.t1_space {α : Type u} {β : Type v} [t1_space β] {f : α β} (hf : embedding f) :
@[protected, instance]
def subtype.t1_space {α : Type u} [t1_space α] {p : α Prop} :
@[protected, instance]
def prod.t1_space {α : Type u} {β : Type v} [t1_space α] [t1_space β] :
t1_space × β)
@[protected, instance]
def pi.t1_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), t1_space (π i)] :
t1_space (Π (i : ι), π i)
@[protected, instance]
def t1_space.t0_space {α : Type u} [t1_space α] :
@[simp]
theorem compl_singleton_mem_nhds_iff {α : Type u} [t1_space α] {x y : α} :
{x} nhds y y x
theorem compl_singleton_mem_nhds {α : Type u} [t1_space α] {x y : α} (h : y x) :
{x} nhds y
@[simp]
theorem closure_singleton {α : Type u} [t1_space α] {a : α} :
closure {a} = {a}
theorem set.subsingleton.closure {α : Type u} [t1_space α] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem subsingleton_closure {α : Type u} [t1_space α] {s : set α} :
theorem is_closed_map_const {α : Type u_1} {β : Type u_2} [t1_space β] {y : β} :
theorem nhds_within_insert_of_ne {α : Type u} [t1_space α] {x y : α} {s : set α} (hxy : x y) :
s) = s
theorem insert_mem_nhds_within_of_subset_insert {α : Type u} [t1_space α] {x y : α} {s t : set α} (hu : t ) :
t

If `t` is a subset of `s`, except for one point, then `insert x s` is a neighborhood of `x` within `t`.

theorem bInter_basis_nhds {α : Type u} [t1_space α] {ι : Sort u_1} {p : ι Prop} {s : ι set α} {x : α} (h : (nhds x).has_basis p s) :
( (i : ι) (h : p i), s i) = {x}
@[simp]
theorem compl_singleton_mem_nhds_set_iff {α : Type u} [t1_space α] {x : α} {s : set α} :
{x} x s
@[simp]
theorem nhds_set_le_iff {α : Type u} [t1_space α] {s t : set α} :
s t
@[simp]
theorem nhds_set_inj_iff {α : Type u} [t1_space α] {s t : set α} :
s = t
theorem injective_nhds_set {α : Type u} [t1_space α] :
theorem strict_mono_nhds_set {α : Type u} [t1_space α] :
@[simp]
theorem nhds_le_nhds_set_iff {α : Type u} [t1_space α] {s : set α} {x : α} :
nhds x x s
theorem dense.diff_singleton {α : Type u} [t1_space α] {s : set α} (hs : dense s) (x : α) [ {x}).ne_bot] :
dense (s \ {x})

Removing a non-isolated point from a dense set, one still obtains a dense set.

theorem dense.diff_finset {α : Type u} [t1_space α] [ (x : α), {x}).ne_bot] {s : set α} (hs : dense s) (t : finset α) :
dense (s \ t)

Removing a finset from a dense set in a space without isolated points, one still obtains a dense set.

theorem dense.diff_finite {α : Type u} [t1_space α] [ (x : α), {x}).ne_bot] {s : set α} (hs : dense s) {t : set α} (ht : t.finite) :
dense (s \ t)

Removing a finite set from a dense set in a space without isolated points, one still obtains a dense set.

theorem eq_of_tendsto_nhds {α : Type u} {β : Type v} [t1_space β] {f : α β} {a : α} {b : β} (h : (nhds a) (nhds b)) :
f a = b

If a function to a `t1_space` tends to some limit `b` at some point `a`, then necessarily `b = f a`.

theorem filter.tendsto.eventually_ne {β : Type v} [t1_space β] {α : Type u_1} {g : α β} {l : filter α} {b₁ b₂ : β} (hg : (nhds b₁)) (hb : b₁ b₂) :
∀ᶠ (z : α) in l, g z b₂
theorem continuous_at.eventually_ne {α : Type u} {β : Type v} [t1_space β] {g : α β} {a : α} {b : β} (hg1 : a) (hg2 : g a b) :
∀ᶠ (z : α) in nhds a, g z b
theorem continuous_at_of_tendsto_nhds {α : Type u} {β : Type v} [t1_space β] {f : α β} {a : α} {b : β} (h : (nhds a) (nhds b)) :

To prove a function to a `t1_space` is continuous at some point `a`, it suffices to prove that `f` admits some limit at `a`.

@[simp]
theorem tendsto_const_nhds_iff {α : Type u} {β : Type v} [t1_space α] {l : filter β} [l.ne_bot] {c d : α} :
filter.tendsto (λ (x : β), c) l (nhds d) c = d
theorem is_open_singleton_of_finite_mem_nhds {α : Type u_1} [t1_space α] (x : α) {s : set α} (hs : s nhds x) (hsf : s.finite) :

A point with a finite neighborhood has to be isolated.

theorem infinite_of_mem_nhds {α : Type u_1} [t1_space α] (x : α) [hx : {x}).ne_bot] {s : set α} (hs : s nhds x) :

If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is infinite.

theorem discrete_of_t1_of_finite {X : Type u_1} [t1_space X] [finite X] :
theorem is_preconnected.infinite_of_nontrivial {α : Type u} [t1_space α] {s : set α} (h : is_preconnected s) (hs : s.nontrivial) :
theorem connected_space.infinite {α : Type u} [nontrivial α] [t1_space α] :
theorem singleton_mem_nhds_within_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
{x} s
theorem nhds_within_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :

The neighbourhoods filter of `x` within `s`, under the discrete topology, is equal to the pure `x` filter (which is the principal filter at the singleton `{x}`.)

theorem filter.has_basis.exists_inter_eq_singleton_of_mem_discrete {α : Type u} {ι : Type u_1} {p : ι Prop} {t : ι set α} {s : set α} {x : α} (hb : (nhds x).has_basis p t) (hx : x s) :
(i : ι) (hi : p i), t i s = {x}
theorem nhds_inter_eq_singleton_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
(U : set α) (H : U nhds x), U s = {x}

A point `x` in a discrete subset `s` of a topological space admits a neighbourhood that only meets `s` at `x`.

theorem disjoint_nhds_within_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
(U : set α) (H : U {x}), s

For point `x` in a discrete subset `s` of a topological space, there is a set `U` such that

1. `U` is a punctured neighborhood of `x` (ie. `U ∪ {x}` is a neighbourhood of `x`),
2. `U` is disjoint from `s`.
theorem topological_space.subset_trans {X : Type u_1} [tX : topological_space X] {s t : set X} (ts : t s) :

Let `X` be a topological space and let `s, t ⊆ X` be two subsets. If there is an inclusion `t ⊆ s`, then the topological space structure on `t` induced by `X` is the same as the one obtained by the induced topological space structure on `s`.

@[class]
structure t2_space (α : Type u)  :
Prop

A T₂ space, also known as a Hausdorff space, is one in which for every `x ≠ y` there exists disjoint open sets around `x` and `y`. This is the most widely used of the separation axioms.

Instances of this typeclass
theorem t2_space_iff (α : Type u)  :
(x y : α), x y ( (u v : set α), x u y v v)
theorem t2_separation {α : Type u} [t2_space α] {x y : α} (h : x y) :
(u v : set α), x u y v v

Two different points can be separated by open sets.

theorem t2_space_iff_disjoint_nhds {α : Type u}  :
(x y : α), x y disjoint (nhds x) (nhds y)
@[simp]
theorem disjoint_nhds_nhds {α : Type u} [t2_space α] {x y : α} :
disjoint (nhds x) (nhds y) x y
theorem pairwise_disjoint_nhds {α : Type u} [t2_space α] :
@[protected]
theorem set.pairwise_disjoint_nhds {α : Type u} [t2_space α] (s : set α) :
theorem set.finite.t2_separation {α : Type u} [t2_space α] {s : set α} (hs : s.finite) :
(U : α set α), ( (x : α), x U x is_open (U x))

Points of a finite set can be separated by open sets from each other.

theorem is_open_set_of_disjoint_nhds_nhds {α : Type u}  :
is_open {p : α × α | disjoint (nhds p.fst) (nhds p.snd)}
@[protected, instance]
def t2_space.t1_space {α : Type u} [t2_space α] :
theorem t2_iff_nhds {α : Type u}  :
{x y : α}, (nhds x nhds y).ne_bot x = y

A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.

theorem eq_of_nhds_ne_bot {α : Type u} [t2_space α] {x y : α} (h : (nhds x nhds y).ne_bot) :
x = y
theorem t2_space_iff_nhds {α : Type u}  :
{x y : α}, x y ( (U : set α) (H : U nhds x) (V : set α) (H : V nhds y), V)
theorem t2_separation_nhds {α : Type u} [t2_space α] {x y : α} (h : x y) :
(u v : set α), u nhds x v nhds y v
theorem t2_separation_compact_nhds {α : Type u} [t2_space α] {x y : α} (h : x y) :
(u v : set α), u nhds x v nhds y v
theorem t2_iff_ultrafilter {α : Type u}  :
{x y : α} (f : , f nhds x f nhds y x = y
theorem t2_iff_is_closed_diagonal {α : Type u}  :
theorem is_closed_diagonal {α : Type u} [t2_space α] :
theorem finset_disjoint_finset_opens_of_t2 {α : Type u} [t2_space α] (s t : finset α) :
t
theorem point_disjoint_finset_opens_of_t2 {α : Type u} [t2_space α] {x : α} {s : finset α} (h : x s) :
s
theorem tendsto_nhds_unique {α : Type u} {β : Type v} [t2_space α] {f : β α} {l : filter β} {a b : α} [l.ne_bot] (ha : (nhds a)) (hb : (nhds b)) :
a = b
theorem tendsto_nhds_unique' {α : Type u} {β : Type v} [t2_space α] {f : β α} {l : filter β} {a b : α} (hl : l.ne_bot) (ha : (nhds a)) (hb : (nhds b)) :
a = b
theorem tendsto_nhds_unique_of_eventually_eq {α : Type u} {β : Type v} [t2_space α] {f g : β α} {l : filter β} {a b : α} [l.ne_bot] (ha : (nhds a)) (hb : (nhds b)) (hfg : f =ᶠ[l] g) :
a = b
theorem tendsto_nhds_unique_of_frequently_eq {α : Type u} {β : Type v} [t2_space α] {f g : β α} {l : filter β} {a b : α} (ha : (nhds a)) (hb : (nhds b)) (hfg : ∃ᶠ (x : β) in l, f x = g x) :
a = b
@[class]
structure t2_5_space (α : Type u)  :
Prop

A T₂.₅ space, also known as a Urysohn space, is a topological space where for every pair `x ≠ y`, there are two open sets, with the intersection of closures empty, one containing `x` and the other `y` .

Instances of this typeclass
@[simp]
theorem disjoint_lift'_closure_nhds {α : Type u} [t2_5_space α] {x y : α} :
@[protected, instance]
def t2_5_space.t2_space {α : Type u} [t2_5_space α] :
theorem exists_nhds_disjoint_closure {α : Type u} [t2_5_space α] {x y : α} (h : x y) :
(s : set α) (H : s nhds x) (t : set α) (H : t nhds y), disjoint (closure s) (closure t)
theorem exists_open_nhds_disjoint_closure {α : Type u} [t2_5_space α] {x y : α} (h : x y) :
(u : set α), x u (v : set α), y v disjoint (closure u) (closure v)

### Properties of `Lim` and `lim`#

In this section we use explicit `nonempty α` instances for `Lim` and `lim`. This way the lemmas are useful without a `nonempty α` instance.

theorem Lim_eq {α : Type u} [t2_space α] {f : filter α} {a : α} [f.ne_bot] (h : f nhds a) :
Lim f = a
theorem Lim_eq_iff {α : Type u} [t2_space α] {f : filter α} [f.ne_bot] (h : (a : α), f nhds a) {a : α} :
Lim f = a f nhds a
theorem ultrafilter.Lim_eq_iff_le_nhds {α : Type u} [t2_space α] {x : α} {F : ultrafilter α} :
F.Lim = x F nhds x
theorem is_open_iff_ultrafilter' {α : Type u} [t2_space α] (U : set α) :
(F : , F.Lim U U F.to_filter
theorem filter.tendsto.lim_eq {α : Type u} {β : Type v} [t2_space α] {a : α} {f : filter β} [f.ne_bot] {g : β α} (h : (nhds a)) :
lim f g = a
theorem filter.lim_eq_iff {α : Type u} {β : Type v} [t2_space α] {f : filter β} [f.ne_bot] {g : β α} (h : (a : α), (nhds a)) {a : α} :
lim f g = a (nhds a)
theorem continuous.lim_eq {α : Type u} {β : Type v} [t2_space α] {f : β α} (h : continuous f) (a : β) :
lim (nhds a) f = f a
@[simp]
theorem Lim_nhds {α : Type u} [t2_space α] (a : α) :
Lim (nhds a) = a
@[simp]
theorem lim_nhds_id {α : Type u} [t2_space α] (a : α) :
lim (nhds a) id = a
@[simp]
theorem Lim_nhds_within {α : Type u} [t2_space α] {a : α} {s : set α} (h : a ) :
Lim s) = a
@[simp]
theorem lim_nhds_within_id {α : Type u} [t2_space α] {a : α} {s : set α} (h : a ) :
lim s) id = a

### `t2_space` constructions #

We use two lemmas to prove that various standard constructions generate Hausdorff spaces from Hausdorff spaces:

• `separated_by_continuous` says that two points `x y : α` can be separated by open neighborhoods provided that there exists a continuous map `f : α → β` with a Hausdorff codomain such that `f x ≠ f y`. We use this lemma to prove that topological spaces defined using `induced` are Hausdorff spaces.

• `separated_by_open_embedding` says that for an open embedding `f : α → β` of a Hausdorff space `α`, the images of two distinct points `x y : α`, `x ≠ y` can be separated by open neighborhoods. We use this lemma to prove that topological spaces defined using `coinduced` are Hausdorff spaces.

@[protected, instance]
def discrete_topology.to_t2_space {α : Type u_1}  :
theorem separated_by_continuous {α : Type u_1} {β : Type u_2} [t2_space β] {f : α β} (hf : continuous f) {x y : α} (h : f x f y) :
(u v : set α), x u y v v
theorem separated_by_open_embedding {α : Type u_1} {β : Type u_2} [t2_space α] {f : α β} (hf : open_embedding f) {x y : α} (h : x y) :
(u v : set β), f x u f y v v
@[protected, instance]
def subtype.t2_space {α : Type u_1} {p : α Prop} [t : topological_space α] [t2_space α] :
@[protected, instance]
def prod.t2_space {α : Type u_1} {β : Type u_2} [t₁ : topological_space α] [t2_space α] [t₂ : topological_space β] [t2_space β] :
t2_space × β)
theorem embedding.t2_space {α : Type u} {β : Type v} [t2_space β] {f : α β} (hf : embedding f) :
@[protected, instance]
def sum.t2_space {α : Type u_1} {β : Type u_2} [t₁ : topological_space α] [t2_space α] [t₂ : topological_space β] [t2_space β] :
t2_space β)
@[protected, instance]
def Pi.t2_space {α : Type u_1} {β : α Type v} [t₂ : Π (a : α), topological_space (β a)] [ (a : α), t2_space (β a)] :
t2_space (Π (a : α), β a)
@[protected, instance]
def sigma.t2_space {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] [ (a : ι), t2_space (α a)] :
t2_space (Σ (i : ι), α i)
theorem is_closed_eq {α : Type u} {β : Type v} [t2_space α] {f g : β α} (hf : continuous f) (hg : continuous g) :
is_closed {x : β | f x = g x}
theorem is_open_ne_fun {α : Type u} {β : Type v} [t2_space α] {f g : β α} (hf : continuous f) (hg : continuous g) :
is_open {x : β | f x g x}
theorem set.eq_on.closure {α : Type u} {β : Type v} [t2_space α] {s : set β} {f g : β α} (h : g s) (hf : continuous f) (hg : continuous g) :
g (closure s)

If two continuous maps are equal on `s`, then they are equal on the closure of `s`. See also `set.eq_on.of_subset_closure` for a more general version.

theorem continuous.ext_on {α : Type u} {β : Type v} [t2_space α] {s : set β} (hs : dense s) {f g : β α} (hf : continuous f) (hg : continuous g) (h : g s) :
f = g

If two continuous functions are equal on a dense set, then they are equal.

theorem eq_on_closure₂' {α : Type u} {β : Type v} {γ : Type u_1} [t2_space α] {s : set β} {t : set γ} {f g : β γ α} (h : (x : β), x s (y : γ), y t f x y = g x y) (hf₁ : (x : β), continuous (f x)) (hf₂ : (y : γ), continuous (λ (x : β), f x y)) (hg₁ : (x : β), continuous (g x)) (hg₂ : (y : γ), continuous (λ (x : β), g x y)) (x : β) (H : x ) (y : γ) (H_1 : y ) :
f x y = g x y
theorem eq_on_closure₂ {α : Type u} {β : Type v} {γ : Type u_1} [t2_space α] {s : set β} {t : set γ} {f g : β γ α} (h : (x : β), x s (y : γ), y t f x y = g x y) (hf : continuous ) (hg : continuous ) (x : β) (H : x ) (y : γ) (H_1 : y ) :
f x y = g x y
theorem set.eq_on.of_subset_closure {α : Type u} {β : Type v} [t2_space α] {s t : set β} {f g : β α} (h : g s) (hf : t) (hg : t) (hst : s t) (hts : t ) :
g t

If `f x = g x` for all `x ∈ s` and `f`, `g` are continuous on `t`, `s ⊆ t ⊆ closure s`, then `f x = g x` for all `x ∈ t`. See also `set.eq_on.closure`.

theorem function.left_inverse.closed_range {α : Type u} {β : Type v} [t2_space α] {f : α β} {g : β α} (h : g) (hf : continuous f) (hg : continuous g) :
theorem function.left_inverse.closed_embedding {α : Type u} {β : Type v} [t2_space α] {f : α β} {g : β α} (h : g) (hf : continuous f) (hg : continuous g) :
theorem is_compact_is_compact_separated {α : Type u} [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : t) :
theorem is_compact.is_closed {α : Type u} [t2_space α] {s : set α} (hs : is_compact s) :

In a `t2_space`, every compact set is closed.

@[simp]
theorem exists_subset_nhds_of_is_compact {α : Type u} [t2_space α] {ι : Type u_1} [nonempty ι] {V : ι set α} (hV : V) (hV_cpct : (i : ι), is_compact (V i)) {U : set α} (hU : (x : α), (x (i : ι), V i) U nhds x) :
(i : ι), V i U

If `V : ι → set α` is a decreasing family of compact sets then any neighborhood of `⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhd_of_compact'` where we don't need to assume each `V i` closed because it follows from compactness since `α` is assumed to be Hausdorff.

theorem compact_exhaustion.is_closed {α : Type u} [t2_space α] (K : compact_exhaustion α) (n : ) :
theorem is_compact.inter {α : Type u} [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :
theorem is_compact_closure_of_subset_compact {α : Type u} [t2_space α] {s t : set α} (ht : is_compact t) (h : s t) :
@[simp]
theorem exists_compact_superset_iff {α : Type u} [t2_space α] {s : set α} :
( (K : set α), s K)
theorem image_closure_of_is_compact {α : Type u} {β : Type v} [t2_space β] {s : set α} (hs : is_compact (closure s)) {f : α β} (hf : (closure s)) :
f '' = closure (f '' s)
theorem is_compact.binary_compact_cover {α : Type u} [t2_space α] {K U V : set α} (hK : is_compact K) (hU : is_open U) (hV : is_open V) (h2K : K U V) :
(K₁ K₂ : set α), K₁ U K₂ V K = K₁ K₂

If a compact set is covered by two open sets, then we can cover it by two compact subsets.

@[protected]
theorem continuous.is_closed_map {α : Type u} {β : Type v} [t2_space β] {f : α β} (h : continuous f) :

A continuous map from a compact space to a Hausdorff space is a closed map.

theorem continuous.closed_embedding {α : Type u} {β : Type v} [t2_space β] {f : α β} (h : continuous f) (hf : function.injective f) :

An injective continuous map from a compact space to a Hausdorff space is a closed embedding.

theorem quotient_map.of_surjective_continuous {α : Type u} {β : Type v} [t2_space β] {f : α β} (hsurj : function.surjective f) (hcont : continuous f) :

A surjective continuous map from a compact space to a Hausdorff space is a quotient map.

theorem is_compact.finite_compact_cover {α : Type u} [t2_space α] {s : set α} (hs : is_compact s) {ι : Type u_1} (t : finset ι) (U : ι set α) (hU : (i : ι), i t is_open (U i)) (hsC : s (i : ι) (H : i t), U i) :
(K : ι set α), ( (i : ι), is_compact (K i)) ( (i : ι), K i U i) s = (i : ι) (H : i t), K i

For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`.

theorem locally_compact_of_compact_nhds {α : Type u} [t2_space α] (h : (x : α), (s : set α), s nhds x ) :
@[protected, instance]
def locally_compact_of_compact {α : Type u} [t2_space α]  :
theorem exists_open_with_compact_closure {α : Type u} [t2_space α] (x : α) :
(U : set α), x U

In a locally compact T₂ space, every point has an open neighborhood with compact closure

theorem exists_open_superset_and_is_compact_closure {α : Type u} [t2_space α] {K : set α} (hK : is_compact K) :
(V : set α), K V

In a locally compact T₂ space, every compact set has an open neighborhood with compact closure.

theorem exists_open_between_and_is_compact_closure {α : Type u} [t2_space α] {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set α), K V U

In a locally compact T₂ space, given a compact set `K` inside an open set `U`, we can find a open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is inside `U`.

theorem is_preirreducible_iff_subsingleton {α : Type u} [t2_space α] {S : set α} :
@[protected]
theorem is_preirreducible.subsingleton {α : Type u} [t2_space α] {S : set α} :

Alias of the forward direction of `is_preirreducible_iff_subsingleton`.

theorem is_irreducible_iff_singleton {α : Type u} [t2_space α] {S : set α} :
(x : α), S = {x}

There does not exist a nontrivial preirreducible T₂ space.

theorem regular_space_iff (X : Type u)  :
{s : set X} {a : X}, a s disjoint (nhds_set s) (nhds a)
@[class]
structure regular_space (X : Type u)  :
Prop

A topological space is called a regular space if for any closed set `s` and `a ∉ s`, there exist disjoint open sets `U ⊇ s` and `V ∋ a`. We formulate this condition in terms of `disjoint`ness of filters `𝓝ˢ s` and `𝓝 a`.

Instances of this typeclass
theorem regular_space_tfae (X : Type u)  :
[, (s : set X) (a : X), a disjoint (nhds_set s) (nhds a), (a : X) (s : set X), disjoint (nhds_set s) (nhds a) a , (a : X) (s : set X), s nhds a ( (t : set X) (H : t nhds a), t s), (a : X), (nhds a).lift' closure nhds a, (a : X), (nhds a).lift' closure = nhds a].tfae
theorem regular_space.of_lift'_closure {α : Type u} (h : (a : α), (nhds a).lift' closure = nhds a) :
theorem regular_space.of_basis {α : Type u} {ι : α Sort u_1} {p : Π (a : α), ι a Prop} {s : Π (a : α), ι a set α} (h₁ : (a : α), (nhds a).has_basis (p a) (s a)) (h₂ : (a : α) (i : ι a), p a i is_closed (s a i)) :
theorem regular_space.of_exists_mem_nhds_is_closed_subset {α : Type u} (h : (a : α) (s : set α), s nhds a ( (t : set α) (H : t nhds a), t s)) :
theorem disjoint_nhds_set_nhds {α : Type u} {a : α} {s : set α} :
theorem disjoint_nhds_nhds_set {α : Type u} {a : α} {s : set α} :
theorem exists_mem_nhds_is_closed_subset {α : Type u} {a : α} {s : set α} (h : s nhds a) :
(t : set α) (H : t nhds a), t s
theorem closed_nhds_basis {α : Type u} (a : α) :
(nhds a).has_basis (λ (s : set α), s nhds a id
theorem lift'_nhds_closure {α : Type u} (a : α) :
theorem filter.has_basis.nhds_closure {α : Type u} {ι : Sort u_1} {a : α} {p : ι Prop} {s : ι set α} (h : (nhds a).has_basis p s) :
(nhds a).has_basis p (λ (i : ι), closure (s i))
theorem has_basis_nhds_closure {α : Type u} (a : α) :
(nhds a).has_basis (λ (s : set α), s nhds a) closure
theorem has_basis_opens_closure {α : Type u} (a : α) :
(nhds a).has_basis (λ (s : set α), a s is_open s) closure
theorem topological_space.is_topological_basis.nhds_basis_closure {α : Type u} {B : set (set α)} (a : α) :
(nhds a).has_basis (λ (s : set α), a s s B) closure
theorem topological_space.is_topological_basis.exists_closure_subset {α : Type u} {B : set (set α)} {a : α} {s : set α} (h : s nhds a) :
(t : set α) (H : t B), a t s
theorem disjoint_nhds_nhds_iff_not_specializes {α : Type u} {a b : α} :
disjoint (nhds a) (nhds b) ¬a b
theorem specializes_comm {α : Type u} {a b : α} :
a b b a
theorem specializes.symm {α : Type u} {a b : α} :
a b b a

Alias of the forward direction of `specializes_comm`.

theorem specializes_iff_inseparable {α : Type u} {a b : α} :
a b b
theorem is_closed_set_of_specializes {α : Type u}  :
is_closed {p : α × α | p.fst p.snd}
theorem is_closed_set_of_inseparable {α : Type u}  :
is_closed {p : α × α | p.snd}
@[protected]
theorem inducing.regular_space {α : Type u} {β : Type v} {f : β α} (hf : inducing f) :
theorem regular_space_induced {α : Type u} {β : Type v} (f : β α) :
theorem regular_space_Inf {X : Type u_1} {T : set } (h : (t : , t T ) :
theorem regular_space_infi {ι : Sort u_1} {X : Type u_2} {t : ι } (h : (i : ι), ) :
theorem regular_space.inf {X : Type u_1} {t₁ t₂ : topological_space X} (h₁ : regular_space X) (h₂ : regular_space X) :
@[protected, instance]
def subtype.regular_space {α : Type u} {p : α Prop} :
@[protected, instance]
def prod.regular_space {α : Type u} {β : Type v}  :
@[protected, instance]
def pi.regular_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), regular_space (π i)] :
regular_space (Π (i : ι), π i)
@[class]
structure t3_space (α : Type u)  :
Prop
• to_t0_space :
• to_regular_space :

A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and a T₂.₅ space.

Instances of this typeclass
@[protected, instance]
def t3_space.t2_5_space {α : Type u} [t3_space α] :
@[protected]
theorem embedding.t3_space {α : Type u} {β : Type v} [t3_space β] {f : α β} (hf : embedding f) :
@[protected, instance]
def subtype.t3_space {α : Type u} [t3_space α] {p : α Prop} :
@[protected, instance]
def prod.t3_space {α : Type u} {β : Type v} [t3_space α] [t3_space β] :
t3_space × β)
@[protected, instance]
def pi.t3_space {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [ (i : ι), t3_space (π i)] :
t3_space (Π (i : ι), π i)
theorem disjoint_nested_nhds {α : Type u} [t3_space α] {x y : α} (h : x y) :
(U₁ : set α) (H : U₁ nhds x) (V₁ : set α) (H : V₁ nhds x) (U₂ : set α) (H : U₂ nhds y) (V₂ : set α) (H : V₂ nhds y), is_open U₁ is_open U₂ V₁ U₁ V₂ U₂ disjoint U₁ U₂

Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`, with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint.

@[protected, instance]

The `separation_quotient` of a regular space is a T₃ space.

@[class]
structure normal_space (α : Type u)  :
Prop

A T₄ space, also known as a normal space (although this condition sometimes omits T₂), is one in which for every pair of disjoint closed sets `C` and `D`, there exist disjoint open sets containing `C` and `D` respectively.

Instances of this typeclass
theorem normal_separation {α : Type u} [normal_space α] {s t : set α} (H1 : is_closed s) (H2 : is_closed t) (H3 : t) :
theorem normal_exists_closure_subset {α : Type u} [normal_space α] {s t : set α} (hs : is_closed s) (ht : is_open t) (hst : s t) :
(u : set α), s u t
@[protected, instance]
def normal_space.t3_space {α : Type u} [normal_space α] :
theorem normal_of_compact_t2 {α : Type u} [t2_space α] :
@[protected]
theorem closed_embedding.normal_space {α : Type u} {β : Type v} [normal_space β] {f : α β} (hf : closed_embedding f) :
@[protected, instance]

The `separation_quotient` of a normal space is a T₄ space. We don't have separate typeclasses for normal spaces (without T₁ assumption) and T₄ spaces, so we use the same class for assumption and for conclusion.

One can prove this using a homeomorphism between `α` and `separation_quotient α`. We give an alternative proof that works without assuming that `α` is a T₁ space.

A T₃ topological space with second countable topology is a normal space. This lemma is not an instance to avoid a loop.

@[class]
structure t5_space (α : Type u)  :
Prop

A topological space `α` is a completely normal Hausdorff space if each subspace `s : set α` is a normal Hausdorff space. Equivalently, `α` is a `T₁` space and for any two sets `s`, `t` such that `closure s` is disjoint with `t` and `s` is disjoint with `closure t`, there exist disjoint neighbourhoods of `s` and `t`.

Instances of this typeclass
theorem embedding.t5_space {α : Type u} {β : Type v} [t5_space β] {e : α β} (he : embedding e) :
@[protected, instance]
def subtype.t5_space {α : Type u} [t5_space α] {p : α Prop} :
t5_space {x // p x}

A subspace of a `T₅` space is a `T₅` space.

@[protected, instance]
def t5_space.to_normal_space {α : Type u} [t5_space α] :

A `T₅` space is a `T₄` space.

@[protected, instance]

The `separation_quotient` of a completely normal space is a T₅ space. We don't have separate typeclasses for completely normal spaces (without T₁ assumption) and T₅ spaces, so we use the same class for assumption and for conclusion.

One can prove this using a homeomorphism between `α` and `separation_quotient α`. We give an alternative proof that works without assuming that `α` is a T₁ space.

theorem connected_component_eq_Inter_clopen {α : Type u} [t2_space α] (x : α) :
= (Z : {Z // x Z}), Z

In a compact t2 space, the connected component of a point equals the intersection of all its clopen neighbourhoods.

A T1 space with a clopen basis is totally separated.

theorem compact_t2_tot_disc_iff_tot_sep {α : Type u} [t2_space α]  :

A compact Hausdorff space is totally disconnected if and only if it is totally separated, this is also true for locally compact spaces.

theorem nhds_basis_clopen {α : Type u} [t2_space α] (x : α) :
(nhds x).has_basis (λ (s : set α), x s id
theorem compact_exists_clopen_in_open {α : Type u} [t2_space α] {x : α} {U : set α} (is_open : _root_.is_open U) (memU : x U) :
(V : set α) (hV : , x V V U

Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set.

A locally compact Hausdorff totally disconnected space has a basis with clopen elements.

A locally compact Hausdorff space is totally disconnected if and only if it is totally separated.

@[protected, instance]
def connected_components.t2 {α : Type u} [t2_space α]  :

`connected_components α` is Hausdorff when `α` is Hausdorff and compact