# T₂ and T₂.₅ spaces. #

This file defines the T₂ (Hausdorff) condition, which is the most commonly-used among the various separation axioms, and the related T₂.₅ condition.

## Main definitions #

- `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₂.

See `Mathlib/Topology/Separation/Regular.lean` for regular, T₃, etc. spaces; and `Mathlib/Topology/Separation/GDelta.lean` for the definitions of `PerfectlyNormalSpace` and `T6Space`.

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.

## Main results #

### 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. `Topology.IsEmbedding.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.

## References #

- https://en.wikipedia.org/wiki/Separation_axiom
- [Willard's General Topology][zbMATH02107988]

source
class T2Space (X : Type u) [TopologicalSpace X] :
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.

- t2 : Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

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

Instances

source
theorem t2Space_iff (X : Type u) [TopologicalSpace X] :
T2Space X ↔ Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
source
theorem t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Two different points can be separated by open sets.

source
theorem t2Space_iff_disjoint_nhds {X : Type u_1} [TopologicalSpace X] :
T2Space X ↔ Pairwise fun (x y : X) => Disjoint (nhds x) (nhds y)
source
@[simp]
theorem disjoint_nhds_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} :
Disjoint (nhds x) (nhds y) ↔ x ≠ y
source
theorem pairwise_disjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] :
Pairwise (Function.onFun Disjoint nhds)
source
theorem Set.pairwiseDisjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Set X) :
s.PairwiseDisjoint nhds
source
theorem Set.Finite.t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : s.Finite) :
∃ (U : X → Set 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.

source
@[instance 100]
instance T2Space.t1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
T1Space X
source
@[instance 100]
instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
R1Space X
source
theorem SeparationQuotient.t2Space_iff {X : Type u_1} [TopologicalSpace X] :
T2Space (SeparationQuotient X) ↔ R1Space X
source
instance SeparationQuotient.t2Space {X : Type u_1} [TopologicalSpace X] [R1Space X] :
T2Space (SeparationQuotient X)
source
@[instance 80]
instance instT2SpaceOfR1SpaceOfT0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] [T0Space X] :
T2Space X
source
theorem R1Space.t2Space_iff_t0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] :
T2Space X ↔ T0Space X
source
theorem t2_iff_nhds {X : Type u_1} [TopologicalSpace X] :
T2Space X ↔ ∀ {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y

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

source
theorem eq_of_nhds_neBot {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} (h : (nhds x ⊓ nhds y).NeBot) :
x = y
source
theorem t2Space_iff_nhds {X : Type u_1} [TopologicalSpace X] :
T2Space X ↔ Pairwise fun (x y : X) => ∃ U ∈ nhds x, ∃ V ∈ nhds y, Disjoint U V
source
theorem t2_separation_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
∃ (u : Set X) (v : Set X), u ∈ nhds x ∧ v ∈ nhds y ∧ Disjoint u v
source
theorem t2_separation_compact_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
∃ (u : Set X) (v : Set X), u ∈ nhds x ∧ v ∈ nhds y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
source
theorem t2_iff_ultrafilter {X : Type u_1} [TopologicalSpace X] :
T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y
source
theorem t2_iff_isClosed_diagonal {X : Type u_1} [TopologicalSpace X] :
T2Space X ↔ IsClosed (Set.diagonal X)
source
theorem isClosed_diagonal {X : Type u_1} [TopologicalSpace X] [T2Space X] :
IsClosed (Set.diagonal X)
source
theorem tendsto_nhds_unique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) :
a = b
source
theorem tendsto_nhds_unique' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} :
l.NeBot → ∀ (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)), a = b
source
theorem tendsto_nhds_unique_of_eventuallyEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : f =ᶠ[l] g) :
a = b
source
theorem tendsto_nhds_unique_of_frequently_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a 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
source
theorem IsCompact.nhdsSet_inter_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
nhdsSet (s ∩ t) = nhdsSet s ⊓ nhdsSet 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`.

source
theorem IsCompact.separation_of_notMem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
∃ (U : Set X) (V : Set X), IsOpen U ∧ IsOpen V ∧ 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`.

source
@[deprecated IsCompact.separation_of_notMem (since := "2025-05-23")]
theorem IsCompact.separation_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
∃ (U : Set X) (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Alias of `IsCompact.separation_of_notMem`.

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`.

source
theorem IsCompact.disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
Disjoint (nhdsSet t) (nhds x)

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

source
theorem Set.InjOn.exists_mem_nhdsSet {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ nhds x, InjOn f u) :
∃ t ∈ nhdsSet s, InjOn f 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.

source
theorem Set.InjOn.exists_isOpen_superset {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ nhds x, InjOn f u) :
∃ (t : Set X), IsOpen t ∧ s ⊆ t ∧ InjOn f 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.

source
theorem lim_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Filter X} {x : X} [f.NeBot] (h : f ≤ nhds x) :
lim f = x
source
theorem lim_eq_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Filter X} [f.NeBot] (h : ∃ (x : X), f ≤ nhds x) {x : X} :
lim f = x ↔ f ≤ nhds x
source
theorem Ultrafilter.lim_eq_iff_le_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X} :
F.lim = x ↔ ↑F ≤ nhds x
source
theorem isOpen_iff_ultrafilter' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (U : Set X) :
IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
source
theorem Filter.Tendsto.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {x : X} {f : Filter Y} [f.NeBot] {g : Y → X} (h : Tendsto g f (nhds x)) :
limUnder f g = x
source
theorem Filter.limUnder_eq_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Filter Y} [f.NeBot] {g : Y → X} (h : ∃ (x : X), Tendsto g f (nhds x)) {x : X} :
limUnder f g = x ↔ Tendsto g f (nhds x)
source
theorem Continuous.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] {f : Y → X} (h : Continuous f) (y : Y) :
limUnder (nhds y) f = f y
source
@[simp]
theorem lim_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) :
lim (nhds x) = x
source
@[simp]
theorem limUnder_nhds_id {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) :
limUnder (nhds x) id = x
source
@[simp]
theorem lim_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Set X} (h : x ∈ closure s) :
lim (nhdsWithin x s) = x
source
@[simp]
theorem limUnder_nhdsWithin_id {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Set X} (h : x ∈ closure s) :
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_isOpenEmbedding` 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.

source
@[instance 100]
instance DiscreteTopology.toT2Space {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] :
T2Space X
source
theorem separated_by_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) {x y : X} (h : f x ≠ f y) :
∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
source
theorem separated_by_isOpenEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : X → Y} (hf : Topology.IsOpenEmbedding f) {x y : X} (h : x ≠ y) :
∃ (u : Set Y) (v : Set Y), IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v
source
instance instT2SpaceSubtype {X : Type u_1} [TopologicalSpace X] {p : X → Prop} [T2Space X] :
T2Space (Subtype p)
source
instance Prod.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] :
T2Space (X × Y)
source
theorem T2Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hinj : Function.Injective f) (hc : Continuous f) :
T2Space X

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

source
theorem Topology.IsEmbedding.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : IsEmbedding f) :
T2Space X

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

source
theorem Homeomorph.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) :
T2Space Y
source
instance ULift.instT2Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
T2Space (ULift.{u_3, u_1} X)
source
instance instT2SpaceSum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] :
T2Space (X ⊕ Y)
source
instance Pi.t2Space {X : Type u_1} {Y : X → Type v} [(a : X) → TopologicalSpace (Y a)] [∀ (a : X), T2Space (Y a)] :
T2Space ((a : X) → Y a)
source
instance Sigma.t2Space {ι : Type u_4} {X : ι → Type u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)] :
T2Space ((i : ι) × X i)
source
def t2Setoid (X : Type u_1) [TopologicalSpace X] :
Setoid X

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

Equations

- t2Setoid X = sInf {s : Setoid X | T2Space (Quotient s)}

Instances For

source
def T2Quotient (X : Type u_1) [TopologicalSpace X] :
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

- T2Quotient X = Quotient (t2Setoid X)

Instances For

source
@[deprecated T2Quotient (since := "2025-05-15")]
def t2Quotient (X : Type u_1) [TopologicalSpace X] :
Type u_1

Alias of `T2Quotient`.

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

Equations

- t2Quotient = T2Quotient

Instances For

source
instance T2Quotient.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] :
TopologicalSpace (T2Quotient X)
Equations

- T2Quotient.instTopologicalSpace = inferInstanceAs (TopologicalSpace (Quotient (t2Setoid X)))

source
def T2Quotient.mk {X : Type u_1} [TopologicalSpace X] :
X → T2Quotient X

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

Equations

- T2Quotient.mk = Quotient.mk (t2Setoid X)

Instances For

source
theorem T2Quotient.mk_eq {X : Type u_1} [TopologicalSpace X] {x y : X} :
mk x = mk y ↔ ∀ (s : Setoid X), T2Space (Quotient s) → s x y
source
theorem T2Quotient.surjective_mk (X : Type u_1) [TopologicalSpace X] :
Function.Surjective mk
source
theorem T2Quotient.continuous_mk (X : Type u_1) [TopologicalSpace X] :
Continuous mk
source
theorem T2Quotient.inductionOn {X : Type u_1} [TopologicalSpace X] {motive : T2Quotient X → Prop} (q : T2Quotient X) (h : ∀ (x : X), motive (mk x)) :
motive q
source
theorem T2Quotient.inductionOn₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {motive : T2Quotient X → T2Quotient Y → Prop} (q : T2Quotient X) (q' : T2Quotient Y) (h : ∀ (x : X) (y : Y), motive (mk x) (mk y)) :
motive q q'
source
instance T2Quotient.instT2Space {X : Type u_1} [TopologicalSpace X] :
T2Space (T2Quotient X)

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

source
theorem T2Quotient.compatible {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) (a b : X) :
a ≈ b → f a = f b
source
def T2Quotient.lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
T2Quotient X → 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 uniqueness is `T2Quotient.unique_lift`.

Equations

- T2Quotient.lift hf = Quotient.lift f ⋯

Instances For

source
theorem T2Quotient.continuous_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
Continuous (lift hf)
source
@[simp]
theorem T2Quotient.lift_mk {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) (x : X) :
lift hf (mk x) = f x
source
theorem T2Quotient.unique_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) {g : T2Quotient X → Y} (hfg : g ∘ mk = f) :
g = lift hf
source
theorem isClosed_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) :
IsClosed {y : Y | f y = g y}
source
theorem IsClosed.isClosed_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f g : X → Y} {s : Set X} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
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.

source
theorem isOpen_ne_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) :
IsOpen {y : Y | f y ≠ g y}
source
theorem Set.EqOn.closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {s : Set Y} {f g : Y → X} (h : EqOn f g s) (hf : Continuous f) (hg : Continuous g) :
EqOn f g (closure s)

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.

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

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

source
theorem eqOn_closure₂' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, 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 ∈ closure s → ∀ y ∈ closure t, f x y = g x y
source
theorem eqOn_closure₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y) (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) (x : X) :
x ∈ closure s → ∀ y ∈ closure t, f x y = g x y
source
theorem Set.EqOn.of_subset_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s t : Set X} {f g : X → Y} (h : EqOn f g s) (hf : ContinuousOn f t) (hg : ContinuousOn g t) (hst : s ⊆ t) (hts : t ⊆ closure s) :
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`.

source
theorem Function.LeftInverse.isClosed_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
IsClosed (Set.range g)
source
theorem Function.LeftInverse.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
Topology.IsClosedEmbedding g
source
theorem SeparatedNhds.of_isCompact_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) :
SeparatedNhds s t
source
theorem SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure s ᶜ)) (H3 : IsClosed t) (H4 : Disjoint s t) :
SeparatedNhds 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`.

source
theorem SeparatedNhds.of_finset_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] (s t : Finset X) (h : Disjoint s t) :
SeparatedNhds ↑s ↑t
source
theorem SeparatedNhds.of_singleton_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) :
SeparatedNhds {x} ↑s
source
theorem IsCompact.isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : IsCompact s) :
IsClosed s

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

source
theorem IsCompact.preimage_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} {s : Set Y} (hs : IsCompact s) (hf : Continuous f) :
IsCompact (f ⁻¹' s)
source
theorem Pi.isCompact_iff {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)] {s : Set ((i : ι) → X i)} :
IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' s)
source
theorem Pi.isCompact_closure_iff {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)] {s : Set ((i : ι) → X i)} :
IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))
source
theorem exists_subset_nhds_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {ι : Type u_4} [Nonempty ι] {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.

source
theorem CompactExhaustion.isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] (K : CompactExhaustion X) (n : ℕ) :
IsClosed (K n)
source
theorem IsCompact.inter {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
IsCompact (s ∩ t)
source
theorem image_closure_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : X → Y} (hf : ContinuousOn f (closure s)) :
f '' closure s = closure (f '' s)
source
theorem ContinuousAt.ne_iff_eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
f x ≠ g x ↔ ∀ᶠ (x : X) in nhds x, f x ≠ g x

Two continuous maps into a Hausdorff space agree at a point iff they agree in a neighborhood.

source
theorem ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) [(nhdsWithin x {x}ᶜ).NeBot] :
f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f =ᶠ[nhds x] g

Local identity principle for continuous maps: Two continuous maps into a Hausdorff space agree in a punctured neighborhood of a non-isolated point iff they agree in a neighborhood.

source
@[deprecated ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (since := "2025-05-22")]
theorem ContinuousAt.eventuallyEq_nhd_iff_eventuallyEq_nhdNE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) [(nhdsWithin x {x}ᶜ).NeBot] :
f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f =ᶠ[nhds x] g

Alias of `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE`.

Local identity principle for continuous maps: Two continuous maps into a Hausdorff space agree in a punctured neighborhood of a non-isolated point iff they agree in a neighborhood.

source
theorem Continuous.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) :
IsClosedMap f

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

source
theorem Continuous.isClosedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) (hf : Function.Injective f) :
Topology.IsClosedEmbedding f

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

source
theorem IsQuotientMap.of_surjective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (hsurj : Function.Surjective f) (hcont : Continuous f) :
Topology.IsQuotientMap f

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

source
theorem isPreirreducible_iff_forall_mem_subset_closure_singleton {X : Type u_1} [TopologicalSpace X] [R1Space X] {S : Set X} :
IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure {x}
source
theorem isPreirreducible_iff_subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} :
IsPreirreducible S ↔ S.Subsingleton
source
theorem IsPreirreducible.subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (h : IsPreirreducible S) :
S.Subsingleton
source
theorem isIrreducible_iff_singleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} :
IsIrreducible S ↔ ∃ (x : X), S = {x}
source
theorem not_preirreducible_nontrivial_t2 (X : Type u_4) [TopologicalSpace X] [PreirreducibleSpace X] [Nontrivial X] [T2Space X] :
False

There does not exist a nontrivial preirreducible T₂ space.

source
theorem t2Space_antitone {X : Type u_4} :
Antitone (@T2Space X)