mathlib3 documentation

topology.category.UniformSpace

The category of uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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!

@[protected, instance]
Equations

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

Equations
@[simp]
@[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 = g f = g
@[protected, instance]

The forgetful functor from uniform spaces to topological spaces.

Equations
structure CpltSepUniformSpace  :
Type (u+1)

A (bundled) complete separated uniform space.

Instances for CpltSepUniformSpace

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