Commit 2026-06-19 10:05 4db60865

View on Github →

chore: move strong measurability proof to setToFun (#40602) The goal is to be able to use the very same lemma for the vector measure integral, in a forthcoming PR.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

added theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subset

Modified Mathlib/MeasureTheory/Integral/Prod.lean

deleted theorem measurableSet_integrable

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.StronglyMeasurable.setToFun_prod_right

added theorem MeasureTheory.setToFun_simpleFunc_eq_setToSimpleFunc

added theorem measurableSet_integrable