Regular, normal, T₃, T₄ and T₅ spaces

This file continues the study of separation properties of topological spaces, focusing on conditions strictly stronger than T₂.

Main definitions

• 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₄.

See 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

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

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

class RegularSpace (X : Type u) [TopologicalSpace X] : Prop

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

• regular {s : Set X} {a : X} : IsClosed s → a ∉ s → Disjoint (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_iff (X : Type u) [TopologicalSpace X] : RegularSpace X ↔ ∀ {s : Set X} {a : X}, IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)

theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] : [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ 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} [TopologicalSpace X] (h : ∀ (x : X), (nhds x).lift' closure ≤ nhds x) : RegularSpace X

theorem RegularSpace.of_lift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), (nhds x).lift' closure = nhds x) : RegularSpace X

theorem RegularSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) : RegularSpace X

theorem RegularSpace.of_exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s) : RegularSpace X

@[instance 100]

instance instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X

A weakly locally compact R₁ space is regular.

theorem disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} : Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s

theorem disjoint_nhds_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} : Disjoint (nhds x) (nhdsSet s) ↔ x ∉ closure s

@[instance 100]

instance instR1Space {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : R1Space X

A regular space is R₁.

theorem exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} (h : s ∈ nhds x) : ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s

theorem closed_nhds_basis {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsClosed s) id

theorem lift'_nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) : (nhds x).lift' closure = nhds x

theorem Filter.HasBasis.nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {ι : 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} [TopologicalSpace X] [RegularSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x) closure

theorem hasBasis_opens_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsOpen s) closure

theorem IsCompact.exists_isOpen_closure_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : U ∈ nhdsSet K) : ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

theorem IsCompact.lift'_closure_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K : Set X} (hK : IsCompact K) : (nhdsSet K).lift' closure = nhdsSet K

theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : IsTopologicalBasis B) (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ s ∈ B) closure

theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ nhds x) : ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s

theorem Topology.IsInducing.regularSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : RegularSpace Y

theorem regularSpace_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] (f : Y → X) : RegularSpace Y

theorem regularSpace_sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, RegularSpace X) : RegularSpace X

theorem regularSpace_iInf {ι : Sort u_3} {X : Type u_4} {t : ι → TopologicalSpace X} (h : ∀ (i : ι), RegularSpace X) : RegularSpace X

theorem RegularSpace.inf {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : RegularSpace X) (h₂ : RegularSpace X) : RegularSpace X

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

instance instRegularSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y)

instance instRegularSpaceForall {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] : RegularSpace ((i : ι) → X i)

theorem SeparatedNhds.of_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : SeparatedNhds s t

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} [TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s) (t_cl : IsClosed t) (st_dis : Disjoint s t) : _root_.HasSeparatingCover 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} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ (L : Set X), IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ 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} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ closure 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.

class T25Space (X : Type u) [TopologicalSpace X] : Prop

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

• t2_5 ⦃x y : X⦄ : x ≠ y → Disjoint ((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} [TopologicalSpace X] [T25Space X] {x y : X} : Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) ↔ x ≠ y

@[instance 100]

instance T25Space.t2Space {X : Type u_1} [TopologicalSpace X] [T25Space X] : T2Space X

theorem exists_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} (h : x ≠ y) : ∃ s ∈ nhds x, ∃ t ∈ nhds y, Disjoint (closure s) (closure t)

theorem exists_open_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} (h : x ≠ y) : ∃ (u : Set X), x ∈ u ∧ IsOpen u ∧ ∃ (v : Set X), y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)

theorem T25Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space Y] {f : X → Y} (hinj : Function.Injective f) (hcont : Continuous f) : T25Space X

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

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

instance Subtype.instT25Space {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : X → Prop} : T25Space { x : X // p x }

class T3Space (X : Type u) [TopologicalSpace X] extends T0Space X, RegularSpace X : Prop

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.

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• regular {s : Set X} {a : X} : IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)

@[instance 90]

instance instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] : T3Space X

theorem RegularSpace.t3Space_iff_t0Space {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : T3Space X ↔ T0Space X

@[instance 100]

instance T3Space.t25Space {X : Type u_1} [TopologicalSpace X] [T3Space X] : T25Space X

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

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

instance Subtype.t3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] {p : X → Prop} : T3Space (Subtype p)

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

instance instT3SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y)

instance instT3SpaceForall {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)] : T3Space ((i : ι) → X i)

theorem disjoint_nested_nhds {X : Type u_1} [TopologicalSpace X] [T3Space 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.

instance instT3SpaceSeparationQuotientOfRegularSpace {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : T3Space (SeparationQuotient X)

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

class NormalSpace (X : Type u) [TopologicalSpace X] : Prop

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) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t

  Two disjoint sets in a normal space admit disjoint neighbourhoods.

theorem normal_separation {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) : SeparatedNhds s t

theorem disjoint_nhdsSet_nhdsSet {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : Disjoint (nhdsSet s) (nhdsSet t)

theorem normal_exists_closure_subset {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ (u : Set X), IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

theorem Topology.IsClosedEmbedding.normalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : NormalSpace X

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

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

@[instance 100]

instance NormalSpace.of_compactSpace_r1Space {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X

@[instance 100]

instance NormalSpace.of_regularSpace_lindelofSpace {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LindelofSpace X] : NormalSpace X

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][zbMATH02107988] (without the assumption of Hausdorff).

@[instance 100]

instance NormalSpace.of_regularSpace_secondCountableTopology {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : NormalSpace X

class T4Space (X : Type u) [TopologicalSpace X] extends T1Space X, NormalSpace X : Prop

A T₄ space is a normal T₁ space.

• t1 (x : X) : IsClosed {x}
• normal (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t

@[instance 100]

instance instT4SpaceOfT1SpaceOfNormalSpace {X : Type u_1} [TopologicalSpace X] [T1Space X] [NormalSpace X] : T4Space X

@[instance 100]

instance T4Space.t3Space {X : Type u_1} [TopologicalSpace X] [T4Space X] : T3Space X

theorem Topology.IsClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space Y] {f : X → Y} (hf : IsClosedEmbedding f) : T4Space X

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

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

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

instance SeparationQuotient.instNormalSpace {X : Type u_1} [TopologicalSpace X] [NormalSpace X] : NormalSpace (SeparationQuotient X)

The SeparationQuotient of a normal space is a normal space.

class CompletelyNormalSpace (X : Type u) [TopologicalSpace X] : Prop

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) t → Disjoint 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.

@[instance 100]

instance CompletelyNormalSpace.toNormalSpace {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] : NormalSpace X

A completely normal space is a normal space.

theorem Topology.IsEmbedding.completelyNormalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompletelyNormalSpace Y] {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X

instance instCompletelyNormalSpaceSubtype {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x : X // p x }

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

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

class T5Space (X : Type u) [TopologicalSpace X] extends T1Space X, CompletelyNormalSpace X : Prop

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

• t1 (x : X) : IsClosed {x}
• completely_normal ⦃s t : Set X⦄ : Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t)

theorem Topology.IsEmbedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : IsEmbedding e) : T5Space X

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

@[instance 100]

instance T5Space.toT4Space {X : Type u_1} [TopologicalSpace X] [T5Space X] : T4Space X

A T₅ space is a T₄ space.

instance instT5SpaceSubtype {X : Type u_1} [TopologicalSpace X] [T5Space X] {p : X → Prop} : T5Space { x : X // p x }

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

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

instance instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] [R0Space X] : T5Space (SeparationQuotient X)

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

theorem connectedComponent_eq_iInter_isClopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (x : X) : connectedComponent x = ⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), ↑s

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

instance ConnectedComponents.t2 {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X)

ConnectedComponents X is Hausdorff when X is Hausdorff and compact