Commit 2024-04-29 16:41 2d739086

View on Github →

feat: generalize iSup_restrict_spanningSets (#12439) The measurability assumption was not necessary. I moved the lemma further down in the file to be able to use restrict_toMeasurable_of_sFinite.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

modified theorem MeasureTheory.Measure.iSup_restrict_spanningSets

added theorem MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet