Theorem MeasureTheory.integral_indicator₂

Modification history

2025-03-03 11:12
Mathlib/MeasureTheory/Integral/Bochner.lean
feat: integrating the integral of an indicator (#22469) …
Added MeasureTheory.integral_indicator₂View on Github →