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]

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

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

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

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

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

• t1 (x : X) : IsClosed {x}
• 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 ↔ T1Space X ∧ CompletelyRegularSpace X

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

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

theorem separatesPoints_continuous_of_t35Space {X : Type u} [TopologicalSpace X] [T1Space X] [T35Space X] : Set.SeparatesPoints Continuous

theorem separatesPoints_continuous_of_t35Space_Icc {X : Type u} [TopologicalSpace X] [T1Space X] [T35Space X] : Set.SeparatesPoints Continuous

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