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 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]
theorem completelyRegularSpace_iff (X : Type u) [] :
∀ (x : X) (K : Set X), xK∃ (f : X), f x = 0 Set.EqOn f 1 K
class CompletelyRegularSpace (X : Type u) [] :

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), xK∃ (f : X), f x = 0 Set.EqOn f 1 K
Instances
theorem CompletelyRegularSpace.completely_regular {X : Type u} [] [self : ] (x : X) (K : Set X) :
xK∃ (f : X), f x = 0 Set.EqOn f 1 K
Equations
• =
instance NormalSpace.instCompletelyRegularSpace {X : Type u} [] [] [] :
Equations
• =
theorem t35Space_iff (X : Type u) [] :
class T35Space (X : Type u) [] extends , :

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

Instances
instance T35Space.instT3space {X : Type u} [] [] [] :
Equations
• =
instance T4Space.instT35Space {X : Type u} [] [] [] :
Equations
• =
theorem injective_stoneCechUnit_of_t35Space {X : Type u} [] [] [] :
Function.Injective stoneCechUnit