Theorem MeasureTheory.setLIntegral_indicator₀

Modification history

2024-10-09 19:21
Mathlib/MeasureTheory/Integral/Lebesgue.lean
feat: `setLintegral` for indicator function and `le_meas` (#15322) …
Added MeasureTheory.setLIntegral_indicator₀View on Github →