Commit 2023-05-22 17:42 e91e8b98

View on Github →

feat: port MeasureTheory.Constructions.BorelSpace.Metrizable (#4222) easy port, only needed to change some names and small proof fixes

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

added theorem aemeasurable_of_tendsto_metrizable_ae'

added theorem aemeasurable_of_tendsto_metrizable_ae

added theorem aemeasurable_of_unif_approx

added theorem measurable_limit_of_tendsto_metrizable_ae

added theorem measurable_of_tendsto_ennreal'

added theorem measurable_of_tendsto_ennreal

added theorem measurable_of_tendsto_metrizable'

added theorem measurable_of_tendsto_metrizable

added theorem measurable_of_tendsto_metrizable_ae

added theorem measurable_of_tendsto_nnreal'

added theorem measurable_of_tendsto_nnreal