Def CpltSepUniformSpace.toUniformSpace

Modification history

2023-06-16 02:09
Mathlib/Topology/Category/UniformSpace.lean
feat: port Topology.Category.UniformSpace (#4531)
Added CpltSepUniformSpace.toUniformSpaceView on Github →