Documentation

Mathlib.Topology.Separation.Regular

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

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

Main definitions #

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:

T₃ spaces #

References #

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 sasDisjoint (nhdsSet s) (nhds a)

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

Instances
theorem regularSpace_iff (X : Type u) [TopologicalSpace X] :
RegularSpace X ∀ {s : Set X} {a : X}, IsClosed sasDisjoint (nhdsSet s) (nhds a)
theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
[RegularSpace X, ∀ (s : Set X), xclosure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) xclosure s, ∀ (x : X), snhds x, tnhds 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_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : XSort u_3} {p : (a : X) → ι aProp} {s : (a : X) → ι aSet X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a iIsClosed (s a i)) :
theorem RegularSpace.of_exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), snhds x, tnhds x, IsClosed t t s) :
@[instance 100]

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) xclosure s
theorem disjoint_nhds_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} :
Disjoint (nhds x) (nhdsSet s) xclosure s
@[instance 100]
instance instR1Space {X : Type u_1} [TopologicalSpace X] [RegularSpace 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) :
tnhds 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 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 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) :
tB, x t closure t s
@[deprecated Topology.IsInducing.regularSpace (since := "2024-10-28")]
theorem Inducing.regularSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] {f : YX} (hf : Topology.IsInducing f) :

Alias of Topology.IsInducing.regularSpace.

theorem regularSpace_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] (f : YX) :
theorem regularSpace_sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (h : tT, RegularSpace X) :
theorem regularSpace_iInf {ι : Sort u_3} {X : Type u_4} {t : ιTopologicalSpace X} (h : ∀ (i : ι), RegularSpace X) :
theorem RegularSpace.inf {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : RegularSpace X) (h₂ : RegularSpace X) :
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) :

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

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

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 .

Instances
@[simp]
@[instance 100]
instance T25Space.t2Space {X : Type u_1} [TopologicalSpace X] [T25Space X] :
theorem exists_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} (h : x y) :
snhds x, tnhds y, Disjoint (closure s) (closure t)
theorem exists_open_nhds_disjoint_closure {X : Type u_1} [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 : XY} (hinj : Function.Injective f) (hcont : Continuous f) :
theorem Topology.IsEmbedding.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space Y] {f : XY} (hf : IsEmbedding f) :
@[deprecated Topology.IsEmbedding.t25Space (since := "2024-10-26")]
theorem Embedding.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space Y] {f : XY} (hf : Topology.IsEmbedding f) :

Alias of Topology.IsEmbedding.t25Space.

theorem Homeomorph.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) :
instance Subtype.instT25Space {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : XProp} :
T25Space { x : X // p x }
@[instance 90]
instance instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] :
@[instance 100]
instance T3Space.t25Space {X : Type u_1} [TopologicalSpace X] [T3Space X] :
theorem Topology.IsEmbedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : XY} (hf : IsEmbedding f) :
@[deprecated Topology.IsEmbedding.t3Space (since := "2024-10-26")]
theorem Embedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : XY} (hf : Topology.IsEmbedding f) :

Alias of Topology.IsEmbedding.t3Space.

theorem Homeomorph.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y) :
instance Subtype.t3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] {p : XProp} :
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.

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

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

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

@[instance 100]

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 T4Space.t3Space {X : Type u_1} [TopologicalSpace X] [T4Space X] :
theorem Topology.IsClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space Y] {f : XY} (hf : IsClosedEmbedding f) :

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

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.

Instances
@[instance 100]

A completely normal space is a normal space.

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

Alias of Topology.IsEmbedding.completelyNormalSpace.

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

theorem Topology.IsEmbedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : IsEmbedding e) :
@[deprecated Topology.IsEmbedding.t5Space (since := "2024-10-26")]
theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : Topology.IsEmbedding e) :

Alias of Topology.IsEmbedding.t5Space.

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

A T₅ space is a T₄ space.

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

A subspace of a T₅ 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.

ConnectedComponents X is Hausdorff when X is Hausdorff and compact

Stacks Tag 0900 (The Stacks entry proves profiniteness.)