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

source
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

Instances

source
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
source
theorem completelyRegularSpace_iff_isOpen {X : Type u} [TopologicalSpace X] :
CompletelyRegularSpace X ↔ ∀ (x : X) (K : Set X), IsOpen K → x ∈ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K ᶜ
source
theorem CompletelyRegularSpace.completely_regular_isOpen {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] (x : X) (K : Set X) :
IsOpen K → x ∈ K → ∃ (f : X → ↑unitInterval), Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K ᶜ
source
instance CompletelyRegularSpace.instRegularSpace {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] :
RegularSpace X
source
instance NormalSpace.instCompletelyRegularSpace {X : Type u} [TopologicalSpace X] [NormalSpace X] [R0Space X] :
CompletelyRegularSpace X
source
theorem Topology.IsInducing.completelyRegularSpace {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] [CompletelyRegularSpace Y] {f : X → Y} (hf : IsInducing f) :
CompletelyRegularSpace X
source
instance instCompletelyRegularSpaceSubtype {X : Type u} [TopologicalSpace X] {p : X → Prop} [CompletelyRegularSpace X] :
CompletelyRegularSpace (Subtype p)
source
theorem completelyRegularSpace_induced {X : Type u_1} {Y : Type u_2} {t : TopologicalSpace Y} (ht : CompletelyRegularSpace Y) (f : X → Y) :
CompletelyRegularSpace X
source
theorem completelyRegularSpace_iInf {ι : Type u_1} {X : Type u_2} {t : ι → TopologicalSpace X} (ht : ∀ (i : ι), CompletelyRegularSpace X) :
CompletelyRegularSpace X
source
theorem completelyRegularSpace_inf {X : Type u_1} {t₁ t₂ : TopologicalSpace X} (ht₁ : CompletelyRegularSpace X) (ht₂ : CompletelyRegularSpace X) :
CompletelyRegularSpace X
source
instance instCompletelyRegularSpaceForall {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)] [ht : ∀ (i : ι), CompletelyRegularSpace (X i)] :
CompletelyRegularSpace ((i : ι) → X i)
source
instance instCompletelyRegularSpaceProd {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : CompletelyRegularSpace X] [htY : CompletelyRegularSpace Y] :
CompletelyRegularSpace (X × Y)
source
theorem isInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] :
Topology.IsInducing stoneCechUnit
source
theorem isDenseInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] :
IsDenseInducing stoneCechUnit
source
theorem completelyRegularSpace_iff_isInducing_stoneCechUnit {X : Type u} [TopologicalSpace X] :
CompletelyRegularSpace X ↔ Topology.IsInducing stoneCechUnit
source
theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] (hX : Cardinal.mk X < Cardinal.continuum) :
TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}
source
class T35Space (X : Type u) [TopologicalSpace X] extends T0Space X, CompletelyRegularSpace X :
Prop

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

- t0 ⦃x y : X⦄ : Inseparable x y → x = y
- 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

source
theorem t35Space_iff (X : Type u) [TopologicalSpace X] :
T35Space X ↔ T0Space X ∧ CompletelyRegularSpace X
source
instance T35Space.instT3space {X : Type u} [TopologicalSpace X] [T35Space X] :
T3Space X
source
instance T4Space.instT35Space {X : Type u} [TopologicalSpace X] [T4Space X] :
T35Space X
source
theorem Topology.IsEmbedding.t35Space {X : Type u} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] [T35Space Y] {f : X → Y} (hf : IsEmbedding f) :
T35Space X
source
instance instT35SpaceSubtype {X : Type u} [TopologicalSpace X] {p : X → Prop} [T35Space X] :
T35Space (Subtype p)
source
instance instT35SpaceForall {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)] [ht : ∀ (i : ι), T35Space (X i)] :
T35Space ((i : ι) → X i)
source
instance instT35SpaceProd {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : T35Space X] [htY : T35Space Y] :
T35Space (X × Y)
source
theorem separatesPoints_continuous_of_t35Space {X : Type u} [TopologicalSpace X] [T35Space X] :
{f : X → ℝ | Continuous f}.SeparatesPoints
source
theorem separatesPoints_continuous_of_t35Space_Icc {X : Type u} [TopologicalSpace X] [T35Space X] :
{f : X → ↑unitInterval | Continuous f}.SeparatesPoints
source
theorem injective_stoneCechUnit_of_t35Space {X : Type u} [TopologicalSpace X] [T35Space X] :
Function.Injective stoneCechUnit
source
theorem isEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] [T35Space X] :
Topology.IsEmbedding stoneCechUnit
source
theorem isDenseEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] [T35Space X] :
IsDenseEmbedding stoneCechUnit
source
theorem t35Space_iff_isEmbedding_stoneCechUnit {X : Type u} [TopologicalSpace X] :
T35Space X ↔ Topology.IsEmbedding stoneCechUnit