mathlib

eb8994b8 - feat(measure_theory): use more `[(pseudo_)metrizable_space]` (#14232)

feat(measure_theory): use more `[(pseudo_)metrizable_space]` (#14232) * Use `[metrizable_space α]` or `[pseudo_metrizable_space α]` assumptions in some lemmas, replace `tendsto_metric` with `tendsto_metrizable` in the names of these lemmas. * Drop `measurable_of_tendsto_metric'` and `measurable_of_tendsto_metric` in favor of `measurable_of_tendsto_metrizable'` and `measurable_of_tendsto_metrizable`.