Mathlib v3 is deprecated. Go to Mathlib v4

Def uniform_space.replace_topology

Modification history

2022-02-15 14:39
src/topology/uniform_space/basic.lean
feat(topology/uniform/uniform_embedding): a sum of two complete spaces is complete (#11971)
Modified uniform_space.replace_topologyView on Github →
2021-11-26 02:32
src/topology/uniform_space/basic.lean
feat(topology): normal topological space with second countable topology is metrizable (#10402) …
Added uniform_space.replace_topologyView on Github →