# Documentation

Mathlib.Topology.CompletelyRegular

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

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