Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-02 14:52 10612383

View on Github →

feat(topology): category of uniform spaces (#1275)

feat(category_theory): uniform spaces
feat(topology/uniform_spaces): CpltSepUniformSpace is a reflective subcategory

Estimated changes

Created src/topology/uniform_space/UniformSpace.lean

added def CpltSepUniformSpace.forget

added def CpltSepUniformSpace.forget_to_Type_via_UniformSpace

added def CpltSepUniformSpace.forget_to_UniformSpace

added def CpltSepUniformSpace.of

added def CpltSepUniformSpace.to_UniformSpace

added structure CpltSepUniformSpace

added def UniformSpace.completion_hom

added theorem UniformSpace.completion_hom_val

added theorem UniformSpace.extension_comp_coe

added theorem UniformSpace.extension_hom_val

added def UniformSpace.forget

added def UniformSpace.forget_to_Top

added def UniformSpace.forget_to_Type_via_Top

added def UniformSpace.of

added def UniformSpace

Modified src/topology/uniform_space/completion.lean

added theorem uniform_space.completion.extension_comp_coe

modified theorem uniform_space.completion.map_id