Commit 2023-09-03 21:10 3f9dee6a

View on Github →

chore: Undo adding a heavy import in MeasureTheory.Integral.Lebesgue. (#6850) Create a new file MeasureTheory.Integral.Indicator to undo adding the import of MeasureTheory.Constructions.BorelSpace.Metrizable in MeasureTheory.Integral.Lebesgue introduced in #6225.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Indicator.lean

added theorem MeasureTheory.tendsto_measure_of_tendsto_indicator

added theorem MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted theorem MeasureTheory.tendsto_measure_of_tendsto_indicator

deleted theorem MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure