mathlib3

600d8eaa - feat(topology/metric_space): define a pseudo metrizable space (#14053)

feat(topology/metric_space): define a pseudo metrizable space (#14053) * define `topological_space.pseudo_metrizable_space`; * copy API from `topological_space.metrizable_space`; * add `pi` instances; * use `X`, `Y` instead of `α`, `β`.