Mathlib v3 is deprecated. Go to Mathlib v4

Theorem embedding.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) …
Modified embedding.metrizable_spaceView on Github →
2022-03-25 18:48
src/topology/metric_space/metrizable.lean
feat(topology/metric_space/metrizable): define and use a metrizable typeclass (#12934)
Added embedding.metrizable_spaceView on Github →