mathlib

005df456 - feat(topology/metric_space): use weaker TC assumptions (#14316)

feat(topology/metric_space): use weaker TC assumptions (#14316) Assume `t0_space` instead of `separated_space` in `metric.of_t0_pseudo_metric_space` and `emetric.of_t0_pseudo_emetric_space` (both definition used to have `t2` in their names).