mathlib documentation

topology.category.UniformSpace

The category of uniform spaces #

We construct the category of uniform spaces, show that the complete separated uniform spaces form a reflective subcategory, and hence possess all limits that uniform spaces do.

TODO: show that uniform spaces actually have all limits!

def UniformSpace  :
Type (u+1)

A (bundled) uniform space.

Equations
@[protected, instance]
Equations
def UniformSpace.of (α : Type u) [uniform_space α] :

Construct a bundled UniformSpace from the underlying type and the typeclass.

Equations
@[simp]
theorem UniformSpace.coe_of (X : Type u) [uniform_space X] :
@[simp]
theorem UniformSpace.coe_comp {X Y Z : UniformSpace} (f : X Y) (g : Y Z) :
(f g) = g f
@[simp]
@[simp]
theorem UniformSpace.coe_mk {X Y : UniformSpace} (f : X → Y) (hf : uniform_continuous f) :
f, hf⟩ = f
theorem UniformSpace.hom_ext {X Y : UniformSpace} {f g : X Y} :
f = gf = g
@[protected, instance]

The forgetful functor from uniform spaces to topological spaces.

Equations
structure CpltSepUniformSpace  :
Type (u+1)

A (bundled) complete separated uniform space.

The function forgetting that a complete separated uniform spaces is complete and separated.

Equations

Construct a bundled UniformSpace from the underlying type and the appropriate typeclasses.

Equations
@[protected, instance]
Equations

The functor turning uniform spaces into complete separated uniform spaces.

Equations