Commit 2026-06-03 07:58 c0ba100f

View on Github →

feat: missing small lemmas in measure theory, cleanup (#40106)

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

added theorem MeasureTheory.AEEqFun.coeFn_const_eq'

added theorem MeasureTheory.AEEqFun.coeFn_finsetProd

added theorem MeasureTheory.AEEqFun.coeFn_fun_finsetProd

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

modified theorem MeasureTheory.integrable_zero

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

added theorem MeasureTheory.Lp.coeFn_finsetSum

added theorem MeasureTheory.Lp.coeFn_fun_finsetSum

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

modified theorem MeasureTheory.AEStronglyMeasurable.div₀

added theorem MeasureTheory.AEStronglyMeasurable.inv₀

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

modified theorem MeasureTheory.StronglyMeasurable.div

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

added theorem MeasureTheory.integral_of_not_completeSpace

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean