Theorem MeasureTheory.setLIntegral_le_meas

Modification history

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