Theorem MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure
Modification history
2024-09-17 15:51
Mathlib/MeasureTheory/Integral/Indicator.lean
chore: remove unnecessary NeBot assumptions (#16847) …
Modified MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasureView on Github →