Theorem measurable_of_tendsto_nnreal'

Modification history

2024-03-09 08:55
Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
feat: `tendsto_of_integral_tendsto_of_monotone` (#11167) …
Deleted measurable_of_tendsto_nnreal'View on Github →
2023-05-22 17:42
Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
feat: port MeasureTheory.Constructions.BorelSpace.Metrizable (#4222) …
Added measurable_of_tendsto_nnreal'View on Github →