Theorem MeasureTheory.withDensity_apply_le

Modification history

2023-11-13 09:12
Mathlib/MeasureTheory/Measure/WithDensity.lean
feat: in a sigma-finite space, `withDensity f s` is the integral of `f` over `s` even if `s` is not measurable (#8377)
Added MeasureTheory.withDensity_apply_leView on Github →