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

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

## Instances

## Equations

- (_ : RegularSpace X) = (_ : RegularSpace X)

## Equations

- (_ : CompletelyRegularSpace X) = (_ : CompletelyRegularSpace X)

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