Theorem MeasureTheory.integral_count

Modification history

2026-03-09 13:45
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat: integrability with respect to a countable sum of measures (#36355) …
Modified MeasureTheory.integral_countView on Github →
2025-04-10 06:23
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat: Bochner integral against the counting measure (#23864) …
Added MeasureTheory.integral_countView on Github →