Documentation

Mathlib.Topology.Separation.Hausdorff

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 for regular, T₃, etc spaces; and Mathlib.Topology.Separation.GDelta 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] :

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

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] :

@[instance 100]

instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space 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] :

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

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] :

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

@[deprecated separated_by_isOpenEmbedding (since := "2024-10-18")]

theorem separated_by_openEmbedding {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

Alias of separated_by_isOpenEmbedding.

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

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

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

@[deprecated Topology.IsEmbedding.t2Space (since := "2024-10-26")]

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

Alias of Topology.IsEmbedding.t2Space.

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} [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] :

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)

Instances For

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] :

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

@[deprecated Function.LeftInverse.isClosedEmbedding (since := "2024-10-20")]

theorem Function.LeftInverse.closedEmbedding {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

Alias of Function.LeftInverse.isClosedEmbedding.

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

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} {π : ι → Type u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} :

IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' 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 (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 : ℕ) :

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 Continuous.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous 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.

@[deprecated Continuous.isClosedEmbedding (since := "2024-10-20")]

theorem Continuous.closedEmbedding {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

Alias of Continuous.isClosedEmbedding.

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.

@[deprecated IsQuotientMap.of_surjective_continuous (since := "2024-10-22")]

theorem QuotientMap.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

Alias of IsQuotientMap.of_surjective_continuous.

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

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

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] :

There does not exist a nontrivial preirreducible T₂ space.

theorem t2Space_antitone {X : Type u_4} :

Antitone (@T2Space X)