Commit 2026-03-05 01:06 592989bd

View on Github →

feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ (#34025) Adds the lemma tendsto_setIntegral_of_monotone₀, a version of tendsto_setIntegral_of_monotone requiring only AEMeasurableSet in the hypotheses. The previous version is redefined as a specialization. Also renames integral_union_ae to setIntegral_union₀ for consistency with the rest of the library (it matches the existing setIntegral_union).

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

deleted theorem MeasureTheory.integral_diff

deleted theorem MeasureTheory.integral_union_ae

added theorem MeasureTheory.setIntegral_diff

added theorem MeasureTheory.setIntegral_diff₀

added theorem MeasureTheory.setIntegral_union₀

added theorem MeasureTheory.tendsto_setIntegral_of_monotone₀