Commit 2022-05-22 16:14 eb8994b8

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.