Theorem measurable_of_tendsto_metrizable_ae

Modification history

2023-05-22 17:42

Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

feat: port MeasureTheory.Constructions.BorelSpace.Metrizable (#4222) …

Added measurable_of_tendsto_metrizable_ae View on Github →