Commit 2023-06-16 02:09 bf2a8908

View on Github →

feat: port Topology.Category.UniformSpace (#4531)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/UniformSpace.lean

added theorem CpltSepUniformSpace.coe_of

added def CpltSepUniformSpace.of

added def CpltSepUniformSpace.toUniformSpace

added structure CpltSepUniformSpace

added theorem UniformSpaceCat.coe_comp

added theorem UniformSpaceCat.coe_id

added theorem UniformSpaceCat.coe_mk

added theorem UniformSpaceCat.coe_of

added def UniformSpaceCat.completionHom

added theorem UniformSpaceCat.completionHom_val

added theorem UniformSpaceCat.extensionHom_val

added theorem UniformSpaceCat.extension_comp_coe

added theorem UniformSpaceCat.hom_ext

added def UniformSpaceCat.of

added def UniformSpaceCat