Mathlib v3 is deprecated. Go to Mathlib v4

Def CpltSepUniformSpace.of

Modification history

2021-02-16 12:05

src/topology/category/UniformSpace.lean

doc(topology/category/*): 5 module docs (#6240) …

Modified CpltSepUniformSpace.of View on Github →

2020-06-24 06:13

src/topology/category/UniformSpace.lean

feat(uniform_space/separation): add separated_set (#3130) …

Modified CpltSepUniformSpace.of View on Github →

2019-08-02 14:52

src/topology/uniform_space/UniformSpace.lean

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

Added CpltSepUniformSpace.of View on Github →