mathlib
0760b201 - feat(topology/metric_space): metrizable spaces (#8759)

Commit

4 years ago

feat(topology/metric_space): metrizable spaces (#8759) Define (pseudo)-metric space constructors for metrizable topological spaces.

Author

PatrickMassot

Parents