Commit 2023-11-07 11:01 18d2099c

View on Github →

feat: add Integrable.piecewise (#8080)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

added theorem MeasureTheory.snormEssSup_piecewise_le

added theorem MeasureTheory.snorm_top_piecewise_le

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Memℒp.piecewise

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.AEStronglyMeasurable.piecewise

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.Integrable.piecewise