Completely regular topological spaces. #

This file defines CompletelyRegularSpace and T35Space.

Main definitions #

Main results #

Completely regular spaces #

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 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 #

theorem completelyRegularSpace_iff (X : Type u) [TopologicalSpace X] :
CompletelyRegularSpace X ∀ (x : X) (K : Set X), IsClosed KxK∃ (f : XunitInterval), Continuous f f x = 0 Set.EqOn f 1 K

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


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