Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pseudo_metric_space.replace_topology_eq

Modification history

2022-05-17 15:34
src/topology/metric_space/basic.lean
feat(topology/metric_space): define a pseudo metrizable space (#14053) …
Added pseudo_metric_space.replace_topology_eqView on Github →