Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 14:15 cb2797ee

View on Github →

feat(measure_theory/constructions/borel_space): drop a countability assumption (#12954)

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

modified theorem ae_measurable_of_tendsto_metric_ae

added theorem measurable_of_tendsto_metrizable'

added theorem measurable_of_tendsto_metrizable