Theorem MeasureTheory.Integrable.summable_of_dirac

Modification history

2026-03-09 13:45
Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean
feat: integrability with respect to a countable sum of measures (#36355) …
Added MeasureTheory.Integrable.summable_of_diracView on Github →