Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inducing.pseudo_metrizable_space

Modification history

2022-05-17 15:34

src/topology/metric_space/metrizable.lean

feat(topology/metric_space): define a pseudo metrizable space (#14053) …

Added inducing.pseudo_metrizable_space View on Github →