mathlib
542d06a6 - feat(measure_theory): use `pseudo_metrizable_space` instead of `metrizable_space` (#14310)

Commit
3 years ago
feat(measure_theory): use `pseudo_metrizable_space` instead of `metrizable_space` (#14310)
Author
Parents
Loading