Theorem MeasureTheory.withDensity_apply'

Modification history

2023-11-14 10:54
Mathlib/MeasureTheory/Measure/WithDensity.lean
feat: s-finite measures (#8405) …
Modified MeasureTheory.withDensity_apply'View on Github →
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'View on Github →