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]

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.

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

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.

theorem t2Space_iff_disjoint_nhds {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ Pairwise fun (x y : X) => Disjoint (nhds x) (nhds y)

@[simp]

theorem disjoint_nhds_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ x ≠ y

theorem pairwise_disjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] : Pairwise (Function.onFun Disjoint nhds)

theorem Set.pairwiseDisjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Set X) : s.PairwiseDisjoint nhds

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.

@[instance 100]

instance T2Space.t1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : T1Space X

@[instance 100]

instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : R1Space X

theorem SeparationQuotient.t2Space_iff {X : Type u_1} [TopologicalSpace X] : T2Space (SeparationQuotient X) ↔ R1Space X

instance SeparationQuotient.t2Space {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space (SeparationQuotient X)

@[instance 80]

instance instT2SpaceOfR1SpaceOfT0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] [T0Space X] : T2Space X

theorem R1Space.t2Space_iff_t0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space X ↔ T0Space X

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.

theorem eq_of_nhds_neBot {X : Type u_1} [TopologicalSpace X] [T2Space X] {x y : X} (h : (nhds x ⊓ nhds y).NeBot) : x = y

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

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

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

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

theorem t2_iff_isClosed_diagonal {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ IsClosed (Set.diagonal X)

theorem isClosed_diagonal {X : Type u_1} [TopologicalSpace X] [T2Space X] : IsClosed (Set.diagonal X)

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

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

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

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

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.

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.

@[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.

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.

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.

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.

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

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

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

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

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

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)

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

@[simp]

theorem lim_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) : lim (nhds x) = x

@[simp]

theorem limUnder_nhds_id {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) : limUnder (nhds x) id = x

@[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

@[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.

@[instance 100]

instance DiscreteTopology.toT2Space {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : T2Space X

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

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

instance instT2SpaceSubtype {X : Type u_1} [TopologicalSpace X] {p : X → Prop} [T2Space X] : T2Space (Subtype p)

instance Prod.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X × Y)

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.

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.

theorem Homeomorph.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y

instance ULift.instT2Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : T2Space (ULift.{u_3, u_1} X)

instance instT2SpaceSum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X ⊕ Y)

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)

instance Sigma.t2Space {ι : Type u_4} {X : ι → Type u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)] : T2Space ((i : ι) × X i)

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)}

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)

@[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

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

Equations

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

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)

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

theorem T2Quotient.surjective_mk (X : Type u_1) [TopologicalSpace X] : Function.Surjective mk

theorem T2Quotient.continuous_mk (X : Type u_1) [TopologicalSpace X] : Continuous mk

theorem T2Quotient.inductionOn {X : Type u_1} [TopologicalSpace X] {motive : T2Quotient X → Prop} (q : T2Quotient X) (h : ∀ (x : X), motive (mk x)) : motive q

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'

instance T2Quotient.instT2Space {X : Type u_1} [TopologicalSpace X] : T2Space (T2Quotient X)

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

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

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 ⋯

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)

@[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

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

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}

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.

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}

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.

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.

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

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

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.

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)

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

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

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.

theorem SeparatedNhds.of_finset_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] (s t : Finset X) (h : Disjoint s t) : SeparatedNhds ↑s ↑t

theorem SeparatedNhds.of_singleton_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : SeparatedNhds {x} ↑s

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.

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)

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)

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

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.

theorem CompactExhaustion.isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] (K : CompactExhaustion X) (n : ℕ) : IsClosed (K n)

theorem IsCompact.inter {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ t)

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)

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.

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.

@[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.

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.

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.

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.

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}

theorem isPreirreducible_iff_subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} : IsPreirreducible S ↔ S.Subsingleton

theorem IsPreirreducible.subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (h : IsPreirreducible S) : S.Subsingleton

theorem isIrreducible_iff_singleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} : IsIrreducible S ↔ ∃ (x : X), S = {x}

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.

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