Completely regular topological spaces. #
Main definitions #
CompletelyRegularSpace: A completely regular space
Xis such that each closed set
K ⊆ Xand a point
x ∈ Kᶜ, there is a continuous function
Xto the unit interval, so that
f x = 0and
f k = 1for 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 #
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
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₃.₅
- [Russell C. Walker, The Stone-Čech Compactification][russell1974]
A space is completely regular if points can be separated from closed sets via continuous functions to the unit interval.