Completely regular topological spaces.

This file defines CompletelyRegularSpace and T35Space.

Main definitions

• CompletelyRegularSpace: A completely regular space X is such that each closed set K ⊆ X and a point x ∈ Kᶜ, there is a continuous function f from X to the unit interval, so that f x = 0 and f k = 1 for all k ∈ K. A completely regular space is a regular space, and a normal space is a completely regular space.
• T35Space: A T₃.₅ space is a completely regular space that is also T₀. A T₃.₅ space is a T₃ space and a T₄ space is a T₃.₅ space.

Main results

Completely regular spaces

• CompletelyRegularSpace.regularSpace: A completely regular space is a regular space.
• NormalSpace.completelyRegularSpace: A normal R0 space is a completely regular space.

T₃.₅ spaces

• T35Space.instT3Space: A T₃.₅ space is a T₃ space.
• T4Space.instT35Space: A T₄ space is a T₃.₅ space.

Implementation notes

The present definition CompletelyRegularSpace is a slight modification of the one given in [russell1974]. There it's assumed that any point x ∈ Kᶜ is separated from the closed set K by a continuous real valued function f (as opposed to f being unit-interval-valued). This can be converted to the present definition by replacing a real-valued f by h ∘ g ∘ f, with g : x ↦ max(x, 0) and h : x ↦ min(x, 1). Some sources (e.g. [russell1974]) also assume that a completely regular space is T₁. Here a completely regular space that is also T₁ is called a T₃.₅ space.

References

• [Russell C. Walker, The Stone-Čech Compactification][russell1974]

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

A space is completely regular if points can be separated from closed sets via continuous functions to the unit interval.

• completely_regular (x : X) (K : Set X) : IsClosed K → x ∉ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K

theorem completelyRegularSpace_iff (X : Type u) [TopologicalSpace X] : CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsClosed K → x ∉ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K

theorem completelyRegularSpace_iff_isOpen {X : Type u} [TopologicalSpace X] : CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsOpen K → x ∈ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 Kᶜ

theorem CompletelyRegularSpace.completely_regular_isOpen {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] (x : X) (K : Set X) : IsOpen K → x ∈ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 Kᶜ

instance CompletelyRegularSpace.instRegularSpace {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] : RegularSpace X

instance NormalSpace.instCompletelyRegularSpace {X : Type u} [TopologicalSpace X] [NormalSpace X] [R0Space X] : CompletelyRegularSpace X

theorem Topology.IsInducing.completelyRegularSpace {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] [CompletelyRegularSpace Y] {f : X → Y} (hf : IsInducing f) : CompletelyRegularSpace X

instance instCompletelyRegularSpaceSubtype {X : Type u} [TopologicalSpace X] {p : X → Prop} [CompletelyRegularSpace X] : CompletelyRegularSpace (Subtype p)

theorem completelyRegularSpace_induced {X : Type u_1} {Y : Type u_2} {t : TopologicalSpace Y} (ht : CompletelyRegularSpace Y) (f : X → Y) : CompletelyRegularSpace X

theorem completelyRegularSpace_iInf {ι : Type u_1} {X : Type u_2} {t : ι → TopologicalSpace X} (ht : ∀ (i : ι), CompletelyRegularSpace X) : CompletelyRegularSpace X

theorem completelyRegularSpace_inf {X : Type u_1} {t₁ t₂ : TopologicalSpace X} (ht₁ : CompletelyRegularSpace X) (ht₂ : CompletelyRegularSpace X) : CompletelyRegularSpace X

instance instCompletelyRegularSpaceForall {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)] [ht : ∀ (i : ι), CompletelyRegularSpace (X i)] : CompletelyRegularSpace ((i : ι) → X i)

instance instCompletelyRegularSpaceProd {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : CompletelyRegularSpace X] [htY : CompletelyRegularSpace Y] : CompletelyRegularSpace (X × Y)

theorem isInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] : Topology.IsInducing stoneCechUnit

theorem isDenseInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] : IsDenseInducing stoneCechUnit

theorem completelyRegularSpace_iff_isInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] : CompletelyRegularSpace X ↔ Topology.IsInducing stoneCechUnit

class T35Space (X : Type u) [TopologicalSpace X] extends T0Space X, CompletelyRegularSpace X : Prop

A T₃.₅ space is a completely regular space that is also T₀.

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• completely_regular (x : X) (K : Set X) : IsClosed K → x ∉ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K

theorem t35Space_iff (X : Type u) [TopologicalSpace X] : T35Space X ↔ T0Space X ∧ CompletelyRegularSpace X

instance T35Space.instT3space {X : Type u} [TopologicalSpace X] [T35Space X] : T3Space X

instance T4Space.instT35Space {X : Type u} [TopologicalSpace X] [T4Space X] : T35Space X

theorem Topology.IsEmbedding.t35Space {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] [T35Space Y] {f : X → Y} (hf : IsEmbedding f) : T35Space X

instance instT35SpaceSubtype {X : Type u} [TopologicalSpace X] {p : X → Prop} [T35Space X] : T35Space (Subtype p)

instance instT35SpaceForall {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)] [ht : ∀ (i : ι), T35Space (X i)] : T35Space ((i : ι) → X i)

instance instT35SpaceProd {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : T35Space X] [htY : T35Space Y] : T35Space (X × Y)

theorem separatesPoints_continuous_of_t35Space {X : Type u} [TopologicalSpace X] [T35Space X] : {f : X → ℝ | Continuous f}.SeparatesPoints

@[deprecated separatesPoints_continuous_of_t35Space (since := "2025-04-13")]

theorem separatesPoints_continuous_of_completelyRegularSpace {X : Type u} [TopologicalSpace X] [T35Space X] : {f : X → ℝ | Continuous f}.SeparatesPoints

Alias of separatesPoints_continuous_of_t35Space.

theorem separatesPoints_continuous_of_t35Space_Icc {X : Type u} [TopologicalSpace X] [T35Space X] : {f : X → ↑unitInterval | Continuous f}.SeparatesPoints

@[deprecated separatesPoints_continuous_of_t35Space_Icc (since := "2025-04-13")]

theorem separatesPoints_continuous_of_completelyRegularSpace_Icc {X : Type u} [TopologicalSpace X] [T35Space X] : {f : X → ↑unitInterval | Continuous f}.SeparatesPoints

Alias of separatesPoints_continuous_of_t35Space_Icc.

theorem injective_stoneCechUnit_of_t35Space {X : Type u} [TopologicalSpace X] [T35Space X] : Function.Injective stoneCechUnit

@[deprecated injective_stoneCechUnit_of_t35Space (since := "2025-04-13")]

theorem injective_stoneCechUnit_of_completelyRegularSpace {X : Type u} [TopologicalSpace X] [T35Space X] : Function.Injective stoneCechUnit

Alias of injective_stoneCechUnit_of_t35Space.

theorem isEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] [T35Space X] : Topology.IsEmbedding stoneCechUnit

theorem isDenseEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] [T35Space X] : IsDenseEmbedding stoneCechUnit

theorem t35Space_iff_isEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] : T35Space X ↔ Topology.IsEmbedding stoneCechUnit