# Separation properties of topological spaces. #

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

## Main definitions #

• SeparatedNhds: Two Sets are separated by neighbourhoods if they are contained in disjoint open sets.
• HasSeparatingCover: A set has a countable cover that can be used with hasSeparatingCovers_iff_separatedNhds to witness when two Sets have SeparatedNhds.
• T0Space: 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.
• R0Space: An R₀ space (sometimes called a symmetric space) is a topological space such that the Specializes relation is symmetric.
• T1Space: 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 (t1Space_iff_exists_open shows that these conditions are equivalent.) T₁ implies T₀ and R₀.
• R1Space: An R₁/preregular space is a space where any two topologically distinguishable points have disjoint neighbourhoods. R₁ implies R₀.
• T2Space: 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. T₂ implies T₁ and R₁.
• T25Space: 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. T₂.₅ implies T₂.
• RegularSpace: A regular space is one where, given any closed C and x ∉ C, there are disjoint open sets containing x and C respectively. Such a space is not necessarily Hausdorff.
• T3Space: A T₃ space is a regular T₀ space. T₃ implies T₂.₅.
• NormalSpace: A normal space, is one where given two disjoint closed sets, we can find two open sets that separate them. Such a space is not necessarily Hausdorff, even if it is T₀.
• T4Space: A T₄ space is a normal T₁ space. T₄ implies T₃.
• CompletelyNormalSpace: A completely normal space is one in which for any two sets s, t such that if both closure s is disjoint with t, and s is disjoint with closure t, then there exist disjoint neighbourhoods of s and t. Embedding.completelyNormalSpace allows us to conclude that this is equivalent to all subspaces being normal. Such a space is not necessarily Hausdorff or regular, even if it is T₀.
• T5Space: A T₅ space is a completely normal T₁ space. T₅ implies T₄.
• PerfectlyNormalSpace: A perfectly normal space is a normal space such that closed sets are Gδ.
• T6Space: A T₆ space is a Perfectly normal T₁ space. T₆ implies T₅.

Note that mathlib adopts the modern convention that m ≤ n if and only if T_m → T_n, but occasionally the literature swaps definitions for e.g. T₃ and regular.

### TODO #

• Add perfectly normal and T6 spaces.
• Use hasSeparatingCovers_iff_separatedNhds to prove that perfectly normal spaces are completely normal.

## Main results #

### T₀ spaces #

• IsClosed.exists_closed_singleton: Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.
• exists_isOpen_singleton_of_isOpen_finite: Given an open finite set S in a T₀ space, there is some x ∈ S such that {x} is open.

### T₁ spaces #

• isClosedMap_const: The constant map is a closed map.
• Finite.instDiscreteTopology: 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_isClosed_diagonal: A space is T₂ iff the diagonal of X (that is, the set of all points of the form (a, a) : X × X) is closed under the product topology.
• separatedNhds_of_finset_finset: Any two disjoint finsets are SeparatedNhds.
• Most topological constructions preserve Hausdorffness; these results are part of the typeclass inference system (e.g. Embedding.t2Space)
• Set.EqOn.closure: If two functions are equal on some set s, they are equal on its closure.
• IsCompact.isClosed: All compact sets are closed.
• WeaklyLocallyCompactSpace.locallyCompactSpace: If a topological space is both weakly locally compact (i.e., each point has a compact neighbourhood) and is T₂, then it is locally compact.
• totallySeparatedSpace_of_t1_of_basis_clopen: If X has a clopen basis, then it is a TotallySeparatedSpace.
• loc_compact_t2_tot_disc_iff_tot_sep: A locally compact T₂ space is totally disconnected iff it is totally separated.
• t2Quotient: the largest T2 quotient of a given topological space.

If the space is also compact:

• normalOfCompactT2: A compact T₂ space is a NormalSpace.
• connectedComponent_eq_iInter_isClopen: The connected component of a point is the intersection of all its clopen neighbourhoods.
• compact_t2_tot_disc_iff_tot_sep: Being a TotallyDisconnectedSpace is equivalent to being a TotallySeparatedSpace.
• ConnectedComponents.t2: ConnectedComponents X is T₂ for X T₂ and compact.

### Regular spaces #

If the space is also Lindelöf:

• NormalSpace.of_regularSpace_lindelofSpace: every regular Lindelöf space is normal.

### 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 #

def SeparatedNhds {X : Type u_1} [] :
Set XSet XProp

SeparatedNhds is a predicate on pairs of subSets of a topological space. It holds if the two subSets are contained in disjoint open sets.

Equations
Instances For
theorem separatedNhds_iff_disjoint {X : Type u_1} [] {s : Set X} {t : Set X} :
theorem SeparatedNhds.disjoint_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} :
Disjoint (nhdsSet s) (nhdsSet t)

Alias of the forward direction of separatedNhds_iff_disjoint.

def HasSeparatingCover {X : Type u_1} [] :
Set XSet XProp

HasSeparatingCovers can be useful witnesses for SeparatedNhds.

Equations
Instances For
theorem hasSeparatingCovers_iff_separatedNhds {X : Type u_1} [] {s : Set X} {t : Set X} :

Used to prove that a regular topological space with Lindelöf topology is a normal space, and (todo) a perfectly normal space is a completely normal space.

theorem Set.hasSeparatingCover_empty_left {X : Type u_1} [] (s : Set X) :
theorem Set.hasSeparatingCover_empty_right {X : Type u_1} [] (s : Set X) :
theorem HasSeparatingCover.mono {X : Type u_1} [] {s₁ : Set X} {s₂ : Set X} {t₁ : Set X} {t₂ : Set X} (sc_st : ) (s_sub : s₁ s₂) (t_sub : t₁ t₂) :
theorem SeparatedNhds.symm {X : Type u_1} [] {s : Set X} {t : Set X} :
theorem SeparatedNhds.comm {X : Type u_1} [] (s : Set X) (t : Set X) :
theorem SeparatedNhds.preimage {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set Y} {t : Set Y} (h : ) (hf : ) :
theorem SeparatedNhds.disjoint {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
theorem SeparatedNhds.disjoint_closure_left {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
theorem SeparatedNhds.disjoint_closure_right {X : Type u_1} [] {s : Set X} {t : Set X} (h : ) :
@[simp]
theorem SeparatedNhds.empty_right {X : Type u_1} [] (s : Set X) :
@[simp]
theorem SeparatedNhds.empty_left {X : Type u_1} [] (s : Set X) :
theorem SeparatedNhds.mono {X : Type u_1} [] {s₁ : Set X} {s₂ : Set X} {t₁ : Set X} {t₂ : Set X} (h : SeparatedNhds s₂ t₂) (hs : s₁ s₂) (ht : t₁ t₂) :
SeparatedNhds s₁ t₁
theorem SeparatedNhds.union_left {X : Type u_1} [] {s : Set X} {t : Set X} {u : Set X} :
SeparatedNhds (s t) u
theorem SeparatedNhds.union_right {X : Type u_1} [] {s : Set X} {t : Set X} {u : Set X} (ht : ) (hu : ) :
class T0Space (X : Type u) [] :

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.

• t0 : ∀ ⦃x y : X⦄, x = y

Two inseparable points in a T₀ space are equal.

Instances
theorem T0Space.t0 {X : Type u} [] [self : ] ⦃x : X ⦃y : X :
x = y

Two inseparable points in a T₀ space are equal.

theorem t0Space_iff_inseparable (X : Type u) [] :
∀ (x y : X), x = y
theorem t0Space_iff_not_inseparable (X : Type u) [] :
Pairwise fun (x y : X) => ¬
theorem Inseparable.eq {X : Type u_1} [] [] {x : X} {y : X} (h : ) :
x = y
theorem Inducing.injective {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

A topology Inducing map from a T₀ space is injective.

theorem Inducing.embedding {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

A topology Inducing map from a T₀ space is a topological embedding.

theorem embedding_iff_inducing {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} :
theorem nhds_injective {X : Type u_1} [] [] :
theorem inseparable_iff_eq {X : Type u_1} [] [] {x : X} {y : X} :
x = y
@[simp]
theorem nhds_eq_nhds_iff {X : Type u_1} [] [] {a : X} {b : X} :
nhds a = nhds b a = b
@[simp]
theorem inseparable_eq_eq {X : Type u_1} [] [] :
Inseparable = Eq
theorem TopologicalSpace.IsTopologicalBasis.inseparable_iff {X : Type u_1} [] {b : Set (Set X)} {x : X} {y : X} :
sb, x s y s
theorem TopologicalSpace.IsTopologicalBasis.eq_iff {X : Type u_1} [] [] {b : Set (Set X)} {x : X} {y : X} :
x = y sb, x s y s
theorem t0Space_iff_exists_isOpen_xor'_mem (X : Type u) [] :
Pairwise fun (x y : X) => ∃ (U : Set X), Xor' (x U) (y U)
theorem exists_isOpen_xor'_mem {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
∃ (U : Set X), Xor' (x U) (y U)
def specializationOrder (X : Type u_3) [] [] :

Specialization forms a partial order on a t0 topological space.

Equations
Instances For
instance SeparationQuotient.instT0Space {X : Type u_1} [] :
Equations
• =
theorem minimal_nonempty_closed_subsingleton {X : Type u_1} [] [] {s : Set X} (hs : ) (hmin : ts, t.Nonemptyt = s) :
s.Subsingleton
theorem minimal_nonempty_closed_eq_singleton {X : Type u_1} [] [] {s : Set X} (hs : ) (hne : s.Nonempty) (hmin : ts, t.Nonemptyt = s) :
∃ (x : X), s = {x}
theorem IsClosed.exists_closed_singleton {X : Type u_1} [] [] [] {S : Set X} (hS : ) (hne : S.Nonempty) :
xS, IsClosed {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 {X : Type u_1} [] [] {s : Set X} (hs : ) (hmin : ts, t.Nonemptyt = s) :
s.Subsingleton
theorem minimal_nonempty_open_eq_singleton {X : Type u_1} [] [] {s : Set X} (hs : ) (hne : s.Nonempty) (hmin : ts, t.Nonemptyt = s) :
∃ (x : X), s = {x}
theorem exists_isOpen_singleton_of_isOpen_finite {X : Type u_1} [] [] {s : Set X} (hfin : s.Finite) (hne : s.Nonempty) (ho : ) :
xs, IsOpen {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_finite {X : Type u_1} [] [] [] [] :
∃ (x : X), IsOpen {x}
theorem t0Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (hf' : ) [] :
theorem Embedding.t0Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :
instance Subtype.t0Space {X : Type u_1} [] [] {p : XProp} :
Equations
• =
theorem t0Space_iff_or_not_mem_closure (X : Type u) [] :
Pairwise fun (a b : X) => aclosure {b} bclosure {a}
instance Prod.instT0Space {X : Type u_1} {Y : Type u_2} [] [] [] [] :
T0Space (X × Y)
Equations
• =
instance Pi.instT0Space {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T0Space (X i)] :
T0Space ((i : ι) → X i)
Equations
• =
instance ULift.instT0Space {X : Type u_1} [] [] :
Equations
• =
theorem T0Space.of_cover {X : Type u_1} [] (h : ∀ (x y : X), ∃ (s : Set X), x s y s T0Space s) :
theorem T0Space.of_open_cover {X : Type u_1} [] (h : ∀ (x : X), ∃ (s : Set X), x s T0Space s) :
theorem r0Space_iff (X : Type u) [] :
Symmetric Specializes
class R0Space (X : Type u) [] :

A topological space is called an R₀ space, if Specializes relation is symmetric.

In other words, given two points x y : X, if every neighborhood of y contains x, then every neighborhood of x contains y.

• specializes_symmetric : Symmetric Specializes

In an R₀ space, the Specializes relation is symmetric.

Instances
theorem R0Space.specializes_symmetric {X : Type u} [] [self : ] :
Symmetric Specializes

In an R₀ space, the Specializes relation is symmetric.

theorem Specializes.symm {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
y x

In an R₀ space, the Specializes relation is symmetric, dot notation version.

theorem specializes_comm {X : Type u_1} [] [] {x : X} {y : X} :
x y y x

In an R₀ space, the Specializes relation is symmetric, Iff version.

theorem specializes_iff_inseparable {X : Type u_1} [] [] {x : X} {y : X} :
x y

In an R₀ space, Specializes is equivalent to Inseparable.

theorem Specializes.inseparable {X : Type u_1} [] [] {x : X} {y : X} :
x y

In an R₀ space, Specializes implies Inseparable.

theorem Inducing.r0Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} (hf : ) :
instance instR0SpaceSubtype {X : Type u_1} [] [] {p : XProp} :
R0Space { x : X // p x }
Equations
• =
instance instR0SpaceProd {X : Type u_1} {Y : Type u_2} [] [] [] [] :
R0Space (X × Y)
Equations
• =
instance instR0SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R0Space (X i)] :
R0Space ((i : ι) → X i)
Equations
• =
theorem isCompact_closure_singleton {X : Type u_1} [] [] {x : X} :

In an R₀ space, the closure of a singleton is a compact set.

theorem Filter.coclosedCompact_le_cofinite {X : Type u_1} [] [] :
Filter.cofinite
def Bornology.relativelyCompact (X : Type u_1) [] [] :

In an R₀ space, relatively compact sets form a bornology. Its cobounded filter is Filter.coclosedCompact. See also Bornology.inCompact the bornology of sets contained in a compact set.

Equations
• = { cobounded' := , le_cofinite' := }
Instances For
theorem Bornology.relativelyCompact.isBounded_iff {X : Type u_1} [] [] {s : Set X} :
theorem Set.Finite.isCompact_closure {X : Type u_1} [] [] {s : Set X} (hs : s.Finite) :

In an R₀ space, the closure of a finite set is a compact set.

class T1Space (X : Type u) [] :

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.

• t1 : ∀ (x : X), IsClosed {x}

A singleton in a T₁ space is a closed set.

Instances
theorem T1Space.t1 {X : Type u} [] [self : ] (x : X) :

A singleton in a T₁ space is a closed set.

theorem isClosed_singleton {X : Type u_1} [] [] {x : X} :
theorem isOpen_compl_singleton {X : Type u_1} [] [] {x : X} :
theorem isOpen_ne {X : Type u_1} [] [] {x : X} :
IsOpen {y : X | y x}
theorem Continuous.isOpen_support {X : Type u_1} {Y : Type u_2} [] [] [Zero X] [] {f : YX} (hf : ) :
theorem Continuous.isOpen_mulSupport {X : Type u_1} {Y : Type u_2} [] [] [One X] [] {f : YX} (hf : ) :
theorem Ne.nhdsWithin_compl_singleton {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
theorem Ne.nhdsWithin_diff_singleton {X : Type u_1} [] [] {x : X} {y : X} (h : x y) (s : Set X) :
nhdsWithin x (s \ {y}) =
theorem nhdsWithin_compl_singleton_le {X : Type u_1} [] [] (x : X) (y : X) :
theorem isOpen_setOf_eventually_nhdsWithin {X : Type u_1} [] [] {p : XProp} :
IsOpen {x : X | ∀ᶠ (y : X) in nhdsWithin x {x}, p y}
theorem Set.Finite.isClosed {X : Type u_1} [] [] {s : Set X} (hs : s.Finite) :
theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne {X : Type u_1} [] [] {b : Set (Set X)} {x : X} {y : X} (h : x y) :
ab, x a ya
theorem Finset.isClosed {X : Type u_1} [] [] (s : ) :
theorem t1Space_TFAE (X : Type u) [] :
[, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}, Continuous CofiniteTopology.of, ∀ ⦃x y : X⦄, x y{y} nhds x, ∀ ⦃x y : X⦄, x ysnhds x, ys, ∀ ⦃x y : X⦄, x y∃ (U : Set X), x U yU, ∀ ⦃x y : X⦄, x yDisjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x yDisjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x yx = y].TFAE
theorem t1Space_iff_continuous_cofinite_of {X : Type u_1} [] :
Continuous CofiniteTopology.of
theorem CofiniteTopology.continuous_of {X : Type u_1} [] [] :
Continuous CofiniteTopology.of
theorem t1Space_iff_exists_open {X : Type u_1} [] :
Pairwise fun (x y : X) => ∃ (U : Set X), x U yU
theorem t1Space_iff_disjoint_pure_nhds {X : Type u_1} [] :
∀ ⦃x y : X⦄, x yDisjoint (pure x) (nhds y)
theorem t1Space_iff_disjoint_nhds_pure {X : Type u_1} [] :
∀ ⦃x y : X⦄, x yDisjoint (nhds x) (pure y)
theorem t1Space_iff_specializes_imp_eq {X : Type u_1} [] :
∀ ⦃x y : X⦄, x yx = y
theorem disjoint_pure_nhds {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
theorem disjoint_nhds_pure {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
theorem Specializes.eq {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
x = y
theorem specializes_iff_eq {X : Type u_1} [] [] {x : X} {y : X} :
x y x = y
@[simp]
theorem specializes_eq_eq {X : Type u_1} [] [] :
(fun (x1 x2 : X) => x1 x2) = Eq
@[simp]
theorem pure_le_nhds_iff {X : Type u_1} [] [] {a : X} {b : X} :
pure a nhds b a = b
@[simp]
theorem nhds_le_nhds_iff {X : Type u_1} [] [] {a : X} {b : X} :
nhds a nhds b a = b
@[instance 100]
instance instR0SpaceOfT1Space {X : Type u_1} [] [] :
Equations
• =
instance instT1SpaceCofiniteTopology {X : Type u_1} :
Equations
• =
theorem continuousWithinAt_update_of_ne {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} {s : Set X} {x : X} {x' : X} {y : Y} (hne : x' x) :
theorem continuousAt_update_of_ne {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} {x : X} {x' : X} {y : Y} (hne : x' x) :
theorem continuousOn_update_iff {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} {s : Set X} {x : X} {y : Y} :
ContinuousOn (Function.update f x y) s ContinuousOn f (s \ {x}) (x sFilter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y))
theorem t1Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (hf' : ) [] :
theorem Embedding.t1Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :
instance Subtype.t1Space {X : Type u} [] [] {p : XProp} :
Equations
• =
instance instT1SpaceProd {X : Type u_1} {Y : Type u_2} [] [] [] [] :
T1Space (X × Y)
Equations
• =
instance instT1SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] :
T1Space ((i : ι) → X i)
Equations
• =
instance ULift.instT1Space {X : Type u_1} [] [] :
Equations
• =
@[instance 100]
instance TotallyDisconnectedSpace.t1Space {X : Type u_1} [] [h : ] :
Equations
• =
@[instance 100]
instance T1Space.t0Space {X : Type u_1} [] [] :
Equations
• =
@[simp]
theorem compl_singleton_mem_nhds_iff {X : Type u_1} [] [] {x : X} {y : X} :
{x} nhds y y x
theorem compl_singleton_mem_nhds {X : Type u_1} [] [] {x : X} {y : X} (h : y x) :
{x} nhds y
@[simp]
theorem closure_singleton {X : Type u_1} [] [] {x : X} :
closure {x} = {x}
theorem Set.Subsingleton.closure {X : Type u_1} [] [] {s : Set X} (hs : s.Subsingleton) :
(closure s).Subsingleton
@[simp]
theorem subsingleton_closure {X : Type u_1} [] [] {s : Set X} :
(closure s).Subsingleton s.Subsingleton
theorem isClosedMap_const {X : Type u_3} {Y : Type u_4} [] [] [] {y : Y} :
theorem nhdsWithin_insert_of_ne {X : Type u_1} [] [] {x : X} {y : X} {s : Set X} (hxy : x y) :
theorem insert_mem_nhdsWithin_of_subset_insert {X : Type u_1} [] [] {x : X} {y : X} {s : Set X} {t : Set X} (hu : t insert y s) :
insert x s

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

@[simp]
theorem ker_nhds {X : Type u_1} [] [] (x : X) :
(nhds x).ker = {x}
theorem biInter_basis_nhds {X : Type u_1} [] [] {ι : Sort u_3} {p : ιProp} {s : ιSet X} {x : X} (h : (nhds x).HasBasis p s) :
⋂ (i : ι), ⋂ (_ : p i), s i = {x}
@[simp]
theorem compl_singleton_mem_nhdsSet_iff {X : Type u_1} [] [] {x : X} {s : Set X} :
{x} xs
@[simp]
theorem nhdsSet_le_iff {X : Type u_1} [] [] {s : Set X} {t : Set X} :
s t
@[simp]
theorem nhdsSet_inj_iff {X : Type u_1} [] [] {s : Set X} {t : Set X} :
= s = t
theorem injective_nhdsSet {X : Type u_1} [] [] :
theorem strictMono_nhdsSet {X : Type u_1} [] [] :
StrictMono nhdsSet
@[simp]
theorem nhds_le_nhdsSet_iff {X : Type u_1} [] [] {s : Set X} {x : X} :
nhds x x s
theorem Dense.diff_singleton {X : Type u_1} [] [] {s : Set X} (hs : ) (x : X) [(nhdsWithin x {x}).NeBot] :
Dense (s \ {x})

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

theorem Dense.diff_finset {X : Type u_1} [] [] [∀ (x : X), (nhdsWithin x {x}).NeBot] {s : Set X} (hs : ) (t : ) :
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 {X : Type u_1} [] [] [∀ (x : X), (nhdsWithin x {x}).NeBot] {s : Set X} (hs : ) {t : Set X} (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 {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) :
f x = y

If a function to a T1Space tends to some limit y at some point x, then necessarily y = f x.

theorem Filter.Tendsto.eventually_ne {Y : Type u_2} {X : Type u_3} [] [] {g : XY} {l : } {b₁ : Y} {b₂ : Y} (hg : Filter.Tendsto g l (nhds b₁)) (hb : b₁ b₂) :
∀ᶠ (z : X) in l, g z b₂
theorem ContinuousAt.eventually_ne {X : Type u_1} {Y : Type u_2} [] [] [] {g : XY} {x : X} {y : Y} (hg1 : ) (hg2 : g x y) :
∀ᶠ (z : X) in nhds x, g z y
theorem eventually_ne_nhds {X : Type u_1} [] [] {a : X} {b : X} (h : a b) :
∀ᶠ (x : X) in nhds a, x b
theorem eventually_ne_nhdsWithin {X : Type u_1} [] [] {a : X} {b : X} {s : Set X} (h : a b) :
∀ᶠ (x : X) in , x b
theorem continuousAt_of_tendsto_nhds {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) :

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

@[simp]
theorem tendsto_const_nhds_iff {X : Type u_1} {Y : Type u_2} [] [] {l : } [l.NeBot] {c : X} {d : X} :
Filter.Tendsto (fun (x : Y) => c) l (nhds d) c = d
theorem isOpen_singleton_of_finite_mem_nhds {X : Type u_1} [] [] (x : X) {s : Set X} (hs : s nhds x) (hsf : s.Finite) :
IsOpen {x}

A point with a finite neighborhood has to be isolated.

theorem infinite_of_mem_nhds {X : Type u_3} [] [] (x : X) [hx : (nhdsWithin x {x}).NeBot] {s : Set X} (hs : s nhds x) :
s.Infinite

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

instance Finite.instDiscreteTopology {X : Type u_1} [] [] [] :
Equations
• =
theorem Set.Finite.continuousOn {X : Type u_1} {Y : Type u_2} [] [] [] {s : Set X} (hs : s.Finite) (f : XY) :
theorem IsPreconnected.infinite_of_nontrivial {X : Type u_1} [] [] {s : Set X} (h : ) (hs : s.Nontrivial) :
s.Infinite
theorem ConnectedSpace.infinite {X : Type u_1} [] [] [] [] :
@[instance 100]
instance ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space {X : Type u_1} [] [] [] [] (x : X) :
(nhdsWithin x {x}).NeBot

A non-trivial connected T1 space has no isolated points.

Equations
• =
theorem IsGδ.compl_singleton {X : Type u_1} [] (x : X) [] :
@[deprecated IsGδ.compl_singleton]
theorem isGδ_compl_singleton {X : Type u_1} [] (x : X) [] :

Alias of IsGδ.compl_singleton.

theorem Set.Countable.isGδ_compl {X : Type u_1} [] {s : Set X} [] (hs : s.Countable) :
theorem Set.Finite.isGδ_compl {X : Type u_1} [] {s : Set X} [] (hs : s.Finite) :
theorem Set.Subsingleton.isGδ_compl {X : Type u_1} [] {s : Set X} [] (hs : s.Subsingleton) :
theorem Finset.isGδ_compl {X : Type u_1} [] [] (s : ) :
IsGδ (↑s)
theorem IsGδ.singleton {X : Type u_1} [] [] (x : X) :
IsGδ {x}
@[deprecated IsGδ.singleton]
theorem isGδ_singleton {X : Type u_1} [] [] (x : X) :
IsGδ {x}

Alias of IsGδ.singleton.

theorem Set.Finite.isGδ {X : Type u_1} [] {s : Set X} [] (hs : s.Finite) :
theorem Set.Subsingleton.isClosed {X : Type u_1} [] [] {A : Set X} (h : A.Subsingleton) :
theorem isClosed_inter_singleton {X : Type u_1} [] [] {A : Set X} {a : X} :
IsClosed (A {a})
theorem isClosed_singleton_inter {X : Type u_1} [] [] {A : Set X} {a : X} :
IsClosed ({a} A)
theorem singleton_mem_nhdsWithin_of_mem_discrete {X : Type u_1} [] {s : Set X} [] {x : X} (hx : x s) :
{x}
theorem nhdsWithin_of_mem_discrete {X : Type u_1} [] {s : Set X} [] {x : X} (hx : x s) :
= pure x

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.HasBasis.exists_inter_eq_singleton_of_mem_discrete {X : Type u_1} [] {ι : Type u_3} {p : ιProp} {t : ιSet X} {s : Set X} [] {x : X} (hb : (nhds x).HasBasis p t) (hx : x s) :
∃ (i : ι), p i t i s = {x}
theorem nhds_inter_eq_singleton_of_mem_discrete {X : Type u_1} [] {s : Set X} [] {x : X} (hx : x s) :
Unhds 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 isOpen_inter_eq_singleton_of_mem_discrete {X : Type u_1} [] {s : Set X} [] {x : X} (hx : x s) :
∃ (U : Set X), U s = {x}

Let x be a point in a discrete subset s of a topological space, then there exists an open set that only meets s at x.

theorem disjoint_nhdsWithin_of_mem_discrete {X : Type u_1} [] {s : Set X} [] {x : X} (hx : x s) :
UnhdsWithin x {x}, Disjoint U 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 closedEmbedding_update {ι : Type u_3} {β : ιType u_4} [] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)] :

### R₁ (preregular) spaces #

theorem r1Space_iff_specializes_or_disjoint_nhds (X : Type u_3) [] :
∀ (x y : X), x y Disjoint (nhds x) (nhds y)
class R1Space (X : Type u_3) [] :

A topological space is called a preregular (a.k.a. R₁) space, if any two topologically distinguishable points have disjoint neighbourhoods.

Instances
theorem R1Space.specializes_or_disjoint_nhds {X : Type u_3} [] [self : ] (x : X) (y : X) :
x y Disjoint (nhds x) (nhds y)
@[instance 100]
instance instR0Space {X : Type u_1} [] [] :
Equations
• =
theorem disjoint_nhds_nhds_iff_not_specializes {X : Type u_1} [] [] {x : X} {y : X} :
Disjoint (nhds x) (nhds y) ¬x y
theorem specializes_iff_not_disjoint {X : Type u_1} [] [] {x : X} {y : X} :
x y ¬Disjoint (nhds x) (nhds y)
theorem disjoint_nhds_nhds_iff_not_inseparable {X : Type u_1} [] [] {x : X} {y : X} :
theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type u_3} [] :
∀ (x y : X), Disjoint (nhds x) (nhds y)
theorem isClosed_setOf_specializes {X : Type u_1} [] [] :
IsClosed {p : X × X | p.1 p.2}
theorem isClosed_setOf_inseparable {X : Type u_1} [] [] :
IsClosed {p : X × X | Inseparable p.1 p.2}
theorem IsCompact.mem_closure_iff_exists_inseparable {X : Type u_1} [] [] {y : X} {K : Set X} (hK : ) :
y xK,

In an R₁ space, a point belongs to the closure of a compact set K if and only if it is topologically inseparable from some point of K.

theorem IsCompact.closure_eq_biUnion_inseparable {X : Type u_1} [] [] {K : Set X} (hK : ) :
= xK, {y : X | }
theorem IsCompact.closure_eq_biUnion_closure_singleton {X : Type u_1} [] [] {K : Set X} (hK : ) :
= xK, closure {x}

In an R₁ space, the closure of a compact set is the union of the closures of its points.

theorem IsCompact.closure_subset_of_isOpen {X : Type u_1} [] [] {K : Set X} (hK : ) {U : Set X} (hU : ) (hKU : K U) :
U

In an R₁ space, if a compact set K is contained in an open set U, then its closure is also contained in U.

theorem IsCompact.closure {X : Type u_1} [] [] {K : Set X} (hK : ) :

The closure of a compact set in an R₁ space is a compact set.

theorem IsCompact.closure_of_subset {X : Type u_1} [] [] {s : Set X} {K : Set X} (hK : ) (h : s K) :
@[deprecated IsCompact.closure_of_subset]
theorem isCompact_closure_of_subset_compact {X : Type u_1} [] [] {s : Set X} {K : Set X} (hK : ) (h : s K) :

Alias of IsCompact.closure_of_subset.

@[simp]
theorem exists_isCompact_superset_iff {X : Type u_1} [] [] {s : Set X} :
(∃ (K : Set X), s K) IsCompact (closure s)
@[deprecated exists_isCompact_superset_iff]
theorem exists_compact_superset_iff {X : Type u_1} [] [] {s : Set X} :
(∃ (K : Set X), s K) IsCompact (closure s)

Alias of exists_isCompact_superset_iff.

theorem SeparatedNhds.of_isCompact_isCompact_isClosed {X : Type u_1} [] [] {K : Set X} {L : Set X} (hK : ) (hL : ) (h'L : ) (hd : Disjoint K L) :

If K and L are disjoint compact sets in an R₁ topological space and L is also closed, then K and L have disjoint neighborhoods.

@[deprecated SeparatedNhds.of_isCompact_isCompact_isClosed]
theorem separatedNhds_of_isCompact_isCompact_isClosed {X : Type u_1} [] [] {K : Set X} {L : Set X} (hK : ) (hL : ) (h'L : ) (hd : Disjoint K L) :

Alias of SeparatedNhds.of_isCompact_isCompact_isClosed.

If K and L are disjoint compact sets in an R₁ topological space and L is also closed, then K and L have disjoint neighborhoods.

theorem IsCompact.binary_compact_cover {X : Type u_1} [] [] {K : Set X} {U : Set X} {V : Set X} (hK : ) (hU : ) (hV : ) (h2K : K U V) :
∃ (K₁ : Set X) (K₂ : Set X), 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.

theorem IsCompact.finite_compact_cover {X : Type u_1} [] [] {s : Set X} (hs : ) {ι : Type u_3} (t : ) (U : ιSet X) (hU : it, IsOpen (U i)) (hsC : s it, U i) :
∃ (K : ιSet X), (∀ (i : ι), IsCompact (K i)) (∀ (i : ι), K i U i) s = it, K i

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

theorem R1Space.of_continuous_specializes_imp {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} (hc : ) (hspec : ∀ (x y : Y), f x f yx y) :
theorem Inducing.r1Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} (hf : ) :
theorem R1Space.induced {X : Type u_1} {Y : Type u_2} [] [] (f : YX) :
instance instR1SpaceSubtype {X : Type u_1} [] [] (p : XProp) :
Equations
• =
theorem R1Space.sInf {X : Type u_3} {T : } (hT : tT, ) :
theorem R1Space.iInf {ι : Type u_3} {X : Type u_4} {t : ι} (ht : ∀ (i : ι), ) :
theorem R1Space.inf {X : Type u_3} {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
instance instR1SpaceProd {X : Type u_1} {Y : Type u_2} [] [] [] [] :
R1Space (X × Y)
Equations
• =
instance instR1SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] :
R1Space ((i : ι) → X i)
Equations
• =
theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} {x : X} {K : Set X} {s : Set Y} (hf : ) (hs : s nhds (f x)) (hKc : ) (hKx : K nhds x) :
Knhds x, Set.MapsTo f K s
@[instance 900]
Equations
• =
theorem IsCompact.isCompact_isClosed_basis_nhds {X : Type u_1} [] [] {x : X} {L : Set X} (hLc : ) (hxL : L nhds x) :
(nhds x).HasBasis (fun (K : Set X) => K nhds x ) fun (x : Set X) => x

If a point in an R₁ space has a compact neighborhood, then it has a basis of compact closed neighborhoods.

@[simp]
theorem Filter.coclosedCompact_eq_cocompact {X : Type u_1} [] [] :

In an R₁ space, the filters coclosedCompact and cocompact are equal.

@[simp]

In an R₁ space, the bornologies relativelyCompact and inCompact are equal.

### Lemmas about a weakly locally compact R₁ space #

In fact, a space with these properties is locally compact and regular. Some lemmas are formulated using the latter assumptions below.

theorem isCompact_isClosed_basis_nhds {X : Type u_1} [] [] (x : X) :
(nhds x).HasBasis (fun (K : Set X) => K nhds x ) fun (x : Set X) => x

In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point x form a basis of neighborhoods of x.

theorem exists_mem_nhds_isCompact_isClosed {X : Type u_1} [] [] (x : X) :
Knhds x,

In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood.

@[instance 80]

A weakly locally compact R₁ space is locally compact.

Equations
• =
theorem exists_isOpen_superset_and_isCompact_closure {X : Type u_1} [] [] {K : Set X} (hK : ) :
∃ (V : Set X), K V IsCompact (closure V)

In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure.

@[deprecated exists_isOpen_superset_and_isCompact_closure]
theorem exists_open_superset_and_isCompact_closure {X : Type u_1} [] [] {K : Set X} (hK : ) :
∃ (V : Set X), K V IsCompact (closure V)

Alias of exists_isOpen_superset_and_isCompact_closure.

In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure.

theorem exists_isOpen_mem_isCompact_closure {X : Type u_1} [] [] (x : X) :
∃ (U : Set X), x U IsCompact (closure U)

In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.

@[deprecated exists_isOpen_mem_isCompact_closure]
theorem exists_open_with_compact_closure {X : Type u_1} [] [] (x : X) :
∃ (U : Set X), x U IsCompact (closure U)

Alias of exists_isOpen_mem_isCompact_closure.

In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.

theorem t2Space_iff (X : Type u) [] :
Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), x u y v Disjoint u v
class T2Space (X : Type u) [] :

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
theorem T2Space.t2 {X : Type u} [] [self : ] :
Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), x u y v Disjoint u v

Every two points in a Hausdorff space admit disjoint open neighbourhoods.

theorem t2_separation {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
∃ (u : Set X) (v : Set X), x u y v Disjoint u v

Two different points can be separated by open sets.

theorem t2Space_iff_disjoint_nhds {X : Type u_1} [] :
Pairwise fun (x y : X) => Disjoint (nhds x) (nhds y)
@[simp]
theorem disjoint_nhds_nhds {X : Type u_1} [] [] {x : X} {y : X} :
Disjoint (nhds x) (nhds y) x y
theorem pairwise_disjoint_nhds {X : Type u_1} [] [] :
Pairwise (Disjoint on nhds)
theorem Set.pairwiseDisjoint_nhds {X : Type u_1} [] [] (s : Set X) :
s.PairwiseDisjoint nhds
theorem Set.Finite.t2_separation {X : Type u_1} [] [] {s : Set X} (hs : s.Finite) :
∃ (U : XSet X), (∀ (x : X), x U x IsOpen (U x)) s.PairwiseDisjoint U

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

@[instance 100]
instance T2Space.t1Space {X : Type u_1} [] [] :
Equations
• =
@[instance 100]
instance T2Space.r1Space {X : Type u_1} [] [] :
Equations
• =
instance SeparationQuotient.t2Space {X : Type u_1} [] [] :
Equations
• =
@[instance 80]
instance instT2SpaceOfR1SpaceOfT0Space {X : Type u_1} [] [] [] :
Equations
• =
theorem R1Space.t2Space_iff_t0Space {X : Type u_1} [] [] :
theorem t2_iff_nhds {X : Type u_1} [] :
∀ {x y : X}, (nhds x nhds y).NeBotx = y

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

theorem eq_of_nhds_neBot {X : Type u_1} [] [] {x : X} {y : X} (h : (nhds x nhds y).NeBot) :
x = y
theorem t2Space_iff_nhds {X : Type u_1} [] :
Pairwise fun (x y : X) => Unhds x, Vnhds y, Disjoint U V
theorem t2_separation_nhds {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
∃ (u : Set X) (v : Set X), u nhds x v nhds y Disjoint u v
theorem t2_separation_compact_nhds {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
∃ (u : Set X) (v : Set X), u nhds x v nhds y Disjoint u v
theorem t2_iff_ultrafilter {X : Type u_1} [] :
∀ {x y : X} (f : ), f nhds xf nhds yx = y
theorem t2_iff_isClosed_diagonal {X : Type u_1} [] :
theorem isClosed_diagonal {X : Type u_1} [] [] :
theorem tendsto_nhds_unique {X : Type u_1} {Y : Type u_2} [] [] {f : YX} {l : } {a : X} {b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) :
a = b
theorem tendsto_nhds_unique' {X : Type u_1} {Y : Type u_2} [] [] {f : YX} {l : } {a : X} {b : X} :
l.NeBotFilter.Tendsto f l (nhds a)Filter.Tendsto f l (nhds b)a = b
theorem tendsto_nhds_unique_of_eventuallyEq {X : Type u_1} {Y : Type u_2} [] [] {f : YX} {g : YX} {l : } {a : X} {b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : f =ᶠ[l] g) :
a = b
theorem tendsto_nhds_unique_of_frequently_eq {X : Type u_1} {Y : Type u_2} [] [] {f : YX} {g : YX} {l : } {a : X} {b : X} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : ∃ᶠ (x : Y) in l, f x = g x) :
a = b
theorem IsCompact.nhdsSet_inter_eq {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
nhdsSet (s t) =

If s and t are compact sets in a T₂ space, then the set neighborhoods filter of s ∩ t is the infimum of set neighborhoods filters for s and t.

For general sets, only the ≤ inequality holds, see nhdsSet_inter_le.

theorem IsCompact.separation_of_not_mem {X : Type u_1} [] [] {x : X} {t : Set X} (H1 : ) (H2 : xt) :
∃ (U : Set X) (V : Set X), t U x V Disjoint U V

In a T2Space X, for a compact set t and a point x outside t, there are open sets U, V that separate t and x.

theorem IsCompact.disjoint_nhdsSet_nhds {X : Type u_1} [] [] {x : X} {t : Set X} (H1 : ) (H2 : xt) :

In a T2Space X, for a compact set t and a point x outside t, 𝓝ˢ t and 𝓝 x are disjoint.

theorem Set.InjOn.exists_mem_nhdsSet {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} {s : Set X} (inj : ) (sc : ) (fc : xs, ) (loc : xs, unhds x, ) :
t,

If a function f is

• injective on a compact set s;
• continuous at every point of this set;
• injective on a neighborhood of each point of this set,

then it is injective on a neighborhood of this set.

theorem Set.InjOn.exists_isOpen_superset {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} {s : Set X} (inj : ) (sc : ) (fc : xs, ) (loc : xs, unhds x, ) :
∃ (t : Set X), s t

If a function f is

• injective on a compact set s;
• continuous at every point of this set;
• injective on a neighborhood of each point of this set,

then it is injective on an open neighborhood of this set.

### Properties of lim and limUnder#

In this section we use explicit Nonempty X instances for lim and limUnder. This way the lemmas are useful without a Nonempty X instance.

theorem lim_eq {X : Type u_1} [] [] {f : } {x : X} [f.NeBot] (h : f nhds x) :
lim f = x
theorem lim_eq_iff {X : Type u_1} [] [] {f : } [f.NeBot] (h : ∃ (x : X), f nhds x) {x : X} :
lim f = x f nhds x
theorem Ultrafilter.lim_eq_iff_le_nhds {X : Type u_1} [] [] [] {x : X} {F : } :
F.lim = x F nhds x
theorem isOpen_iff_ultrafilter' {X : Type u_1} [] [] [] (U : Set X) :
∀ (F : ), F.lim UU F
theorem Filter.Tendsto.limUnder_eq {X : Type u_1} {Y : Type u_2} [] [] {x : X} {f : } [f.NeBot] {g : YX} (h : Filter.Tendsto g f (nhds x)) :
limUnder f g = x
theorem Filter.limUnder_eq_iff {X : Type u_1} {Y : Type u_2} [] [] {f : } [f.NeBot] {g : YX} (h : ∃ (x : X), Filter.Tendsto g f (nhds x)) {x : X} :
theorem Continuous.limUnder_eq {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} (h : ) (y : Y) :
limUnder (nhds y) f = f y
@[simp]
theorem lim_nhds {X : Type u_1} [] [] (x : X) :
lim (nhds x) = x
@[simp]
theorem limUnder_nhds_id {X : Type u_1} [] [] (x : X) :
limUnder (nhds x) id = x
@[simp]
theorem lim_nhdsWithin {X : Type u_1} [] [] {x : X} {s : Set X} (h : x ) :
lim (nhdsWithin x s) = x
@[simp]
theorem limUnder_nhdsWithin_id {X : Type u_1} [] [] {x : X} {s : Set X} (h : x ) :
limUnder (nhdsWithin x s) id = x

### T2Space 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 : X can be separated by open neighborhoods provided that there exists a continuous map f : X → Y 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_openEmbedding says that for an open embedding f : X → Y of a Hausdorff space X, the images of two distinct points x y : X, x ≠ y can be separated by open neighborhoods. We use this lemma to prove that topological spaces defined using coinduced are Hausdorff spaces.

@[instance 100]
instance DiscreteTopology.toT2Space {X : Type u_1} [] [] :
Equations
• =
theorem separated_by_continuous {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) {x : X} {y : X} (h : f x f y) :
∃ (u : Set X) (v : Set X), x u y v Disjoint u v
theorem separated_by_openEmbedding {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) {x : X} {y : X} (h : x y) :
∃ (u : Set Y) (v : Set Y), f x u f y v Disjoint u v
instance instT2SpaceSubtype {X : Type u_1} [] {p : XProp} [] :
Equations
• =
instance Prod.t2Space {X : Type u_1} {Y : Type u_2} [] [] [] [] :
T2Space (X × Y)
Equations
• =
theorem T2Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hinj : ) (hc : ) :

If the codomain of an injective continuous function is a Hausdorff space, then so is its domain.

theorem Embedding.t2Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

If the codomain of a topological embedding is a Hausdorff space, then so is its domain. See also T2Space.of_continuous_injective.

instance ULift.instT2Space {X : Type u_1} [] [] :
Equations
• =
instance instT2SpaceSum {X : Type u_1} {Y : Type u_2} [] [] [] [] :
T2Space (X Y)
Equations
• =
instance Pi.t2Space {X : Type u_1} {Y : XType v} [(a : X) → TopologicalSpace (Y a)] [∀ (a : X), T2Space (Y a)] :
T2Space ((a : X) → Y a)
Equations
• =
instance Sigma.t2Space {ι : Type u_4} {X : ιType u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)] :
T2Space ((i : ι) × X i)
Equations
• =
def t2Setoid (X : Type u_1) [] :

The smallest equivalence relation on a topological space giving a T2 quotient.

Equations
Instances For
def t2Quotient (X : Type u_1) [] :
Type u_1

The largest T2 quotient of a topological space. This construction is left-adjoint to the inclusion of T2 spaces into all topological spaces.

Equations
Instances For
instance t2Quotient.instTopologicalSpace {X : Type u_1} [] :
Equations
• t2Quotient.instTopologicalSpace =
def t2Quotient.mk {X : Type u_1} [] :
X

The map from a topological space to its largest T2 quotient.

Equations
• t2Quotient.mk =
Instances For
theorem t2Quotient.mk_eq {X : Type u_1} [] {x : X} {y : X} :
∀ (s : ), T2Space (Quotient s)s.Rel x y
theorem t2Quotient.surjective_mk (X : Type u_1) [] :
Function.Surjective t2Quotient.mk
theorem t2Quotient.continuous_mk (X : Type u_1) [] :
Continuous t2Quotient.mk
theorem t2Quotient.inductionOn {X : Type u_1} [] {motive : } (q : ) (h : ∀ (x : X), motive ) :
motive q
theorem t2Quotient.inductionOn₂ {X : Type u_1} {Y : Type u_2} [] [] {motive : } (q : ) (q' : ) (h : ∀ (x : X) (y : Y), motive ) :
motive q q'
instance t2Quotient.instT2Space {X : Type u_1} [] :

The largest T2 quotient of a topological space is indeed T2.

Equations
• =
theorem t2Quotient.compatible {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} (hf : ) (a : X) (b : X) :
a bf a = f b
def t2Quotient.lift {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} (hf : ) :
Y

The universal property of the largest T2 quotient of a topological space X: any continuous map from X to a T2 space Y uniquely factors through t2Quotient X. This declaration builds the factored map. Its continuity is t2Quotient.continuous_lift, the fact that it indeed factors the original map is t2Quotient.lift_mk and uniquenes is t2Quotient.unique_lift.

Equations
Instances For
theorem t2Quotient.continuous_lift {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} (hf : ) :
@[simp]
theorem t2Quotient.lift_mk {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} (hf : ) (x : X) :
= f x
theorem t2Quotient.unique_lift {X : Type u_3} {Y : Type u_4} [] [] [] {f : XY} (hf : ) {g : Y} (hfg : g t2Quotient.mk = f) :
g =
theorem isClosed_eq {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} {g : YX} (hf : ) (hg : ) :
IsClosed {y : Y | f y = g y}
theorem IsClosed.isClosed_eq {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {g : XY} {s : Set X} (hs : ) (hf : ) (hg : ) :
IsClosed {x : X | x s f x = g x}

If functions f and g are continuous on a closed set s, then the set of points x ∈ s such that f x = g x is a closed set.

theorem isOpen_ne_fun {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} {g : YX} (hf : ) (hg : ) :
IsOpen {y : Y | f y g y}
theorem Set.EqOn.closure {X : Type u_1} {Y : Type u_2} [] [] [] {s : Set Y} {f : YX} {g : YX} (h : Set.EqOn f g s) (hf : ) (hg : ) :

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

theorem Continuous.ext_on {X : Type u_1} {Y : Type u_2} [] [] [] {s : Set Y} (hs : ) {f : YX} {g : YX} (hf : ) (hg : ) (h : Set.EqOn f g s) :
f = g

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

theorem eqOn_closure₂' {X : Type u_1} {Y : Type u_2} [] {Z : Type u_3} [] [] [] {s : Set X} {t : Set Y} {f : XYZ} {g : XYZ} (h : xs, yt, f x y = g x y) (hf₁ : ∀ (x : X), Continuous (f x)) (hf₂ : ∀ (y : Y), Continuous fun (x : X) => f x y) (hg₁ : ∀ (x : X), Continuous (g x)) (hg₂ : ∀ (y : Y), Continuous fun (x : X) => g x y) (x : X) :
x y, f x y = g x y
theorem eqOn_closure₂ {X : Type u_1} {Y : Type u_2} [] {Z : Type u_3} [] [] [] {s : Set X} {t : Set Y} {f : XYZ} {g : XYZ} (h : xs, yt, f x y = g x y) (hf : ) (hg : ) (x : X) :
x y, f x y = g x y
theorem Set.EqOn.of_subset_closure {X : Type u_1} {Y : Type u_2} [] [] [] {s : Set X} {t : Set X} {f : XY} {g : XY} (h : Set.EqOn f g s) (hf : ) (hg : ) (hst : s t) (hts : t ) :
Set.EqOn f 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.EqOn.closure.

theorem Function.LeftInverse.isClosed_range {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {g : YX} (h : ) (hf : ) (hg : ) :
@[deprecated Function.LeftInverse.isClosed_range]
theorem Function.LeftInverse.closed_range {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {g : YX} (h : ) (hf : ) (hg : ) :

Alias of Function.LeftInverse.isClosed_range.

theorem Function.LeftInverse.closedEmbedding {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} {g : YX} (h : ) (hf : ) (hg : ) :
theorem SeparatedNhds.of_isCompact_isCompact {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hst : Disjoint s t) :
@[deprecated SeparatedNhds.of_isCompact_isCompact]
theorem separatedNhds_of_isCompact_isCompact {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hst : Disjoint s t) :

Alias of SeparatedNhds.of_isCompact_isCompact.

theorem SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed {X : Type u_1} [] [] {s : Set X} {t : Set X} (H1 : ) (H2 : ) (H3 : ) (H4 : Disjoint s t) :

In a T2Space X, for disjoint closed sets s t such that closure sᶜ is compact, there are neighbourhoods that separate s and t.

theorem SeparatedNhds.of_finset_finset {X : Type u_1} [] [] (s : ) (t : ) (h : Disjoint s t) :
SeparatedNhds s t
@[deprecated SeparatedNhds.of_finset_finset]
theorem separatedNhds_of_finset_finset {X : Type u_1} [] [] (s : ) (t : ) (h : Disjoint s t) :
SeparatedNhds s t

Alias of SeparatedNhds.of_finset_finset.

theorem SeparatedNhds.of_singleton_finset {X : Type u_1} [] [] {x : X} {s : } (h : xs) :
SeparatedNhds {x} s
@[deprecated SeparatedNhds.of_singleton_finset]
theorem point_disjoint_finset_opens_of_t2 {X : Type u_1} [] [] {x : X} {s : } (h : xs) :
SeparatedNhds {x} s

Alias of SeparatedNhds.of_singleton_finset.

theorem IsCompact.isClosed {X : Type u_1} [] [] {s : Set X} (hs : ) :

In a T2Space, every compact set is closed.

theorem IsCompact.preimage_continuous {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} {s : Set Y} (hs : ) (hf : ) :
theorem Pi.isCompact_iff {ι : Type u_4} {π : ιType u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} :
∀ (i : ι), IsCompact ( '' s)
theorem Pi.isCompact_closure_iff {ι : Type u_4} {π : ιType u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} :
IsCompact (closure s) ∀ (i : ι), IsCompact (closure ( '' s))
theorem exists_subset_nhds_of_isCompact {X : Type u_1} [] [] {ι : Type u_4} [] {V : ιSet X} (hV : Directed (fun (x1 x2 : Set X) => x1 x2) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) {U : Set X} (hU : x⋂ (i : ι), V i, U nhds x) :
∃ (i : ι), V i U

If V : ι → Set X 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_nhds_of_isCompact' where we don't need to assume each V i closed because it follows from compactness since X is assumed to be Hausdorff.

theorem CompactExhaustion.isClosed {X : Type u_1} [] [] (K : ) (n : ) :
IsClosed (K n)
theorem IsCompact.inter {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
theorem image_closure_of_isCompact {X : Type u_1} {Y : Type u_2} [] [] [] {s : Set X} (hs : IsCompact (closure s)) {f : XY} (hf : ContinuousOn f (closure s)) :
f '' = closure (f '' s)
theorem Continuous.isClosedMap {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} (h : ) :

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

theorem Continuous.closedEmbedding {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} (h : ) (hf : ) :

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

theorem QuotientMap.of_surjective_continuous {X : Type u_1} {Y : Type u_2} [] [] [] [] {f : XY} (hsurj : ) (hcont : ) :

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

theorem isPreirreducible_iff_subsingleton {X : Type u_1} [] [] {S : Set X} :
S.Subsingleton
theorem IsPreirreducible.subsingleton {X : Type u_1} [] [] {S : Set X} (h : ) :
S.Subsingleton
theorem isIrreducible_iff_singleton {X : Type u_1} [] [] {S : Set X} :
∃ (x : X), S = {x}
theorem not_preirreducible_nontrivial_t2 (X : Type u_4) [] [] [] :

There does not exist a nontrivial preirreducible T₂ space.

theorem regularSpace_iff (X : Type u) [] :
∀ {s : Set X} {a : X}, asDisjoint (nhdsSet s) (nhds a)
class RegularSpace (X : Type u) [] :

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 Disjointness of filters 𝓝ˢ s and 𝓝 a.

• regular : ∀ {s : Set X} {a : X}, asDisjoint (nhdsSet s) (nhds a)

If a is a point that does not belong to a closed set s, then a and s admit disjoint neighborhoods.

Instances
theorem RegularSpace.regular {X : Type u} [] [self : ] {s : Set X} {a : X} :
asDisjoint (nhdsSet s) (nhds a)

If a is a point that does not belong to a closed set s, then a and s admit disjoint neighborhoods.

theorem regularSpace_TFAE (X : Type u) [] :
[, ∀ (s : Set X), x, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) x, ∀ (x : X), snhds x, tnhds x, t s, ∀ (x : X), (nhds x).lift' closure nhds x, ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE
theorem RegularSpace.of_lift'_closure_le {X : Type u_1} [] (h : ∀ (x : X), (nhds x).lift' closure nhds x) :
theorem RegularSpace.of_lift'_closure {X : Type u_1} [] (h : ∀ (x : X), (nhds x).lift' closure = nhds x) :
@[deprecated RegularSpace.of_lift'_closure]
theorem RegularSpace.ofLift'_closure {X : Type u_1} [] (h : ∀ (x : X), (nhds x).lift' closure = nhds x) :

Alias of RegularSpace.of_lift'_closure.

theorem RegularSpace.of_hasBasis {X : Type u_1} [] {ι : XSort u_3} {p : (a : X) → ι aProp} {s : (a : X) → ι aSet X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a iIsClosed (s a i)) :
@[deprecated RegularSpace.of_hasBasis]
theorem RegularSpace.ofBasis {X : Type u_1} [] {ι : XSort u_3} {p : (a : X) → ι aProp} {s : (a : X) → ι aSet X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a iIsClosed (s a i)) :

Alias of RegularSpace.of_hasBasis.

theorem RegularSpace.of_exists_mem_nhds_isClosed_subset {X : Type u_1} [] (h : ∀ (x : X), snhds x, tnhds x, t s) :
@[deprecated RegularSpace.of_exists_mem_nhds_isClosed_subset]
theorem RegularSpace.ofExistsMemNhdsIsClosedSubset {X : Type u_1} [] (h : ∀ (x : X), snhds x, tnhds x, t s) :

Alias of RegularSpace.of_exists_mem_nhds_isClosed_subset.

@[instance 100]

A weakly locally compact R₁ space is regular.

Equations
• =
theorem disjoint_nhdsSet_nhds {X : Type u_1} [] [] {x : X} {s : Set X} :
Disjoint (nhdsSet s) (nhds x) x
theorem disjoint_nhds_nhdsSet {X : Type u_1} [] [] {x : X} {s : Set X} :
Disjoint (nhds x) (nhdsSet s) x
@[instance 100]
instance instR1Space {X : Type u_1} [] [] :

A regular space is R₁.

Equations
• =
theorem exists_mem_nhds_isClosed_subset {X : Type u_1} [] [] {x : X} {s : Set X} (h : s nhds x) :
tnhds x, t s
theorem closed_nhds_basis {X : Type u_1} [] [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => s nhds x ) id
theorem lift'_nhds_closure {X : Type u_1} [] [] (x : X) :
(nhds x).lift' closure = nhds x
theorem Filter.HasBasis.nhds_closure {X : Type u_1} [] [] {ι : Sort u_3} {x : X} {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
(nhds x).HasBasis p fun (i : ι) => closure (s i)
theorem hasBasis_nhds_closure {X : Type u_1} [] [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => s nhds x) closure
theorem hasBasis_opens_closure {X : Type u_1} [] [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => x s ) closure
theorem IsCompact.exists_isOpen_closure_subset {X : Type u_1} [] [] {K : Set X} {U : Set X} (hK : ) (hU : U ) :
∃ (V : Set X), K V U
theorem IsCompact.lift'_closure_nhdsSet {X : Type u_1} [] [] {K : Set X} (hK : ) :
(nhdsSet K).lift' closure =
theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {X : Type u_1} [] [] {B : Set (Set X)} (x : X) :
(nhds x).HasBasis (fun (s : Set X) => x s s B) closure
theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {X : Type u_1} [] [] {B : Set (Set X)} {x : X} {s : Set X} (h : s nhds x) :
tB, x t s
theorem Inducing.regularSpace {X : Type u_1} {Y : Type u_2} [] [] [] {f : YX} (hf : ) :
theorem regularSpace_induced {X : Type u_1} {Y : Type u_2} [] [] (f : YX) :
theorem regularSpace_sInf {X : Type u_3} {T : } (h : tT, ) :
theorem regularSpace_iInf {ι : Sort u_3} {X : Type u_4} {t : ι} (h : ∀ (i : ι), ) :
theorem RegularSpace.inf {X : Type u_3} {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
instance instRegularSpaceSubtype {X : Type u_1} [] [] {p : XProp} :
Equations
• =
instance instRegularSpaceProd {X : Type u_1} {Y : Type u_2} [] [] [] [] :
Equations
• =
instance instRegularSpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] :
RegularSpace ((i : ι) → X i)
Equations
• =
theorem SeparatedNhds.of_isCompact_isClosed {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hst : Disjoint s t) :

In a regular space, if a compact set and a closed set are disjoint, then they have disjoint neighborhoods.

@[deprecated SeparatedNhds.of_isCompact_isClosed]
theorem separatedNhds_of_isCompact_isClosed {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hst : Disjoint s t) :

Alias of SeparatedNhds.of_isCompact_isClosed.

In a regular space, if a compact set and a closed set are disjoint, then they have disjoint neighborhoods.

theorem IsClosed.HasSeparatingCover {X : Type u_1} [] {s : Set X} {t : Set X} [] [] (s_cl : ) (t_cl : ) (st_dis : Disjoint s t) :

This technique to witness HasSeparatingCover in regular Lindelöf topological spaces will be used to prove regular Lindelöf spaces are normal.

theorem exists_compact_closed_between {X : Type u_1} [] [] {K : Set X} {U : Set X} (hK : ) (hU : ) (h_KU : K U) :
∃ (L : Set X), K L U

In a (possibly non-Hausdorff) locally compact regular space, for every containment K ⊆ U of a compact set K in an open set U, there is a compact closed neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact closed set L such that K ⊆ interior L and L ⊆ U.

theorem exists_open_between_and_isCompact_closure {X : Type u_1} [] [] {K : Set X} {U : Set X} (hK : ) (hU : ) (hKU : K U) :
∃ (V : Set X), K V U IsCompact (closure V)

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

@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]
theorem locally_compact_of_compact {X : Type u_1} [] [] [] :
class T25Space (X : Type u) [] :

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 .

• t2_5 : ∀ ⦃x y : X⦄, x yDisjoint ((nhds x).lift' closure) ((nhds y).lift' closure)

Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are disjoint.

Instances
theorem T25Space.t2_5 {X : Type u} [] [self : ] ⦃x : X ⦃y : X :
x yDisjoint ((nhds x).lift' closure) ((nhds y).lift' closure)

Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are disjoint.

@[simp]
theorem disjoint_lift'_closure_nhds {X : Type u_1} [] [] {x : X} {y : X} :
Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) x y
@[instance 100]
instance T25Space.t2Space {X : Type u_1} [] [] :
Equations
• =
theorem exists_nhds_disjoint_closure {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
snhds x, tnhds y, Disjoint (closure s) (closure t)
theorem exists_open_nhds_disjoint_closure {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
∃ (u : Set X), x u ∃ (v : Set X), y v Disjoint (closure u) (closure v)
theorem T25Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hinj : ) (hcont : ) :
theorem Embedding.t25Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :
instance Subtype.instT25Space {X : Type u_1} [] [] {p : XProp} :
T25Space { x : X // p x }
Equations
• =
class T3Space (X : Type u) [] extends , :

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
@[instance 90]
instance instT3Space {X : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance T3Space.t25Space {X : Type u_1} [] [] :
Equations
• =
theorem Embedding.t3Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :
instance Subtype.t3Space {X : Type u_1} [] [] {p : XProp} :
Equations
• =
instance ULift.instT3Space {X : Type u_1} [] [] :
Equations
• =
instance instT3SpaceProd {X : Type u_1} {Y : Type u_2} [] [] [] [] :
T3Space (X × Y)
Equations
• =
instance instT3SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)] :
T3Space ((i : ι) → X i)
Equations
• =
theorem disjoint_nested_nhds {X : Type u_1} [] [] {x : X} {y : X} (h : x y) :
U₁nhds x, V₁nhds x, U₂nhds y, V₂nhds y, IsClosed V₁ IsClosed V₂ IsOpen U₁ IsOpen 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.

The SeparationQuotient of a regular space is a T₃ space.

Equations
• =
class NormalSpace (X : Type u) [] :

A topological space is said to be a normal space if any two disjoint closed sets have disjoint open neighborhoods.

• normal : ∀ (s t : Set X), Disjoint s t

Two disjoint sets in a normal space admit disjoint neighbourhoods.

Instances
theorem NormalSpace.normal {X : Type u} [] [self : ] (s : Set X) (t : Set X) :
Disjoint s t

Two disjoint sets in a normal space admit disjoint neighbourhoods.

theorem normal_separation {X : Type u_1} [] [] {s : Set X} {t : Set X} (H1 : ) (H2 : ) (H3 : Disjoint s t) :
theorem disjoint_nhdsSet_nhdsSet {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hd : Disjoint s t) :
theorem normal_exists_closure_subset {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hst : s t) :
∃ (u : Set X), s u t
theorem ClosedEmbedding.normalSpace {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

If the codomain of a closed embedding is a normal space, then so is the domain.

@[instance 100]
instance NormalSpace.of_compactSpace_r1Space {X : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance NormalSpace.of_regularSpace_lindelofSpace {X : Type u_1} [] [] [] :

A regular topological space with a Lindelöf topology is a normal space. A consequence of e.g. Corollaries 20.8 and 20.10 of Willard's General Topology (without the assumption of Hausdorff).

Equations
• =
@[instance 100]
Equations
• =
class T4Space (X : Type u) [] extends , :

A T₄ space is a normal T₁ space.

Instances
@[instance 100]
instance instT4SpaceOfT1SpaceOfNormalSpace {X : Type u_1} [] [] [] :
Equations
• =
@[instance 100]
instance T4Space.t3Space {X : Type u_1} [] [] :
Equations
• =
@[deprecated inferInstance]
theorem T4Space.of_compactSpace_t2Space {X : Type u_1} [] [] [] :
theorem ClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

If the codomain of a closed embedding is a T₄ space, then so is the domain.

instance ULift.instT4Space {X : Type u_1} [] [] :
Equations
• =
instance SeparationQuotient.instNormalSpace {X : Type u_1} [] [] :

The SeparationQuotient of a normal space is a normal space.

Equations
• =
class CompletelyNormalSpace (X : Type u) [] :

A topological space X is a completely normal space provided that for any two sets s, t such that if both closure s is disjoint with t, and s is disjoint with closure t, then there exist disjoint neighbourhoods of s and t.

• completely_normal : ∀ ⦃s t : Set X⦄, Disjoint (closure s) tDisjoint s (closure t)Disjoint (nhdsSet s) (nhdsSet t)

If closure s is disjoint with t, and s is disjoint with closure t, then s and t admit disjoint neighbourhoods.

Instances
theorem CompletelyNormalSpace.completely_normal {X : Type u} [] [self : ] ⦃s : Set X ⦃t : Set X :

If closure s is disjoint with t, and s is disjoint with closure t, then s and t admit disjoint neighbourhoods.

@[instance 100]

A completely normal space is a normal space.

Equations
• =
theorem Embedding.completelyNormalSpace {X : Type u_1} {Y : Type u_2} [] [] {e : XY} (he : ) :
instance instCompletelyNormalSpaceSubtype {X : Type u_1} [] {p : XProp} :
CompletelyNormalSpace { x : X // p x }

A subspace of a completely normal space is a completely normal space.

Equations
• =
instance ULift.instCompletelyNormalSpace {X : Type u_1} [] :
Equations
• =
class T5Space (X : Type u) [] extends , :

A T₅ space is a completely normal T₁ space.

Instances
theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [] [] [] {e : XY} (he : ) :
@[instance 100]
instance T5Space.toT4Space {X : Type u_1} [] [] :

A T₅ space is a T₄ space.

Equations
• =
instance instT5SpaceSubtype {X : Type u_1} [] [] {p : XProp} :
T5Space { x : X // p x }

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

Equations
• =
instance ULift.instT5Space {X : Type u_1} [] [] :
Equations
• =

The SeparationQuotient of a completely normal R₀ space is a T₅ space.

Equations
• =
class PerfectlyNormalSpace (X : Type u) [] extends :

A topological space X is a perfectly normal space provided it is normal and closed sets are Gδ.

• normal : ∀ (s t : Set X), Disjoint s t
• closed_gdelta : ∀ ⦃h : Set X⦄, IsGδ h
Instances
theorem PerfectlyNormalSpace.closed_gdelta {X : Type u} [] [self : ] ⦃h : Set X :
IsGδ h
theorem Disjoint.hasSeparatingCover_closed_gdelta_right {X : Type u_1} [] {s : Set X} {t : Set X} [] (st_dis : Disjoint s t) (t_cl : ) (t_gd : IsGδ t) :

Lemma that allows the easy conclusion that perfectly normal spaces are completely normal.

@[instance 100]
Equations
• =
class T6Space (X : Type u) [] extends , :

A T₆ space is a perfectly normal T₁ space.

Instances
@[instance 100]
instance T6Space.toT5Space {X : Type u_1} [] [] :

A T₆ space is a T₅ space.

Equations
• =
theorem connectedComponent_eq_iInter_isClopen {X : Type u_1} [] [] [] (x : X) :
= ⋂ (s : { s : Set X // x s }), s

In a compact T₂ 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 {X : Type u_1} [] [] [] :

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

@[instance 100]
instance instTotallySeparatedSpace {X : Type u_1} [] [] [] :

A totally disconnected compact Hausdorff space is totally separated.

Equations
• =
theorem nhds_basis_clopen {X : Type u_1} [] [] [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => x s ) id
theorem compact_exists_isClopen_in_isOpen {X : Type u_1} [] [] [] {x : X} {U : Set X} (is_open : ) (memU : x U) :
∃ (V : Set X), 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.

theorem loc_compact_t2_tot_disc_iff_tot_sep {H : Type u_3} [] [] :

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

instance ConnectedComponents.t2 {X : Type u_1} [] [] [] :

ConnectedComponents X is Hausdorff when X is Hausdorff and compact

Equations
• =