Theorem MeasureTheory.sFinite_withDensity_of_sigmaFinite_of_measurable

Modification history

2025-02-01 09:03
Mathlib/MeasureTheory/Measure/WithDensity.lean
chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) …
Deleted MeasureTheory.sFinite_withDensity_of_sigmaFinite_of_measurableView on Github →
2024-05-07 10:24
Mathlib/MeasureTheory/Measure/WithDensity.lean
feat: `withDensity` of an s-finite measure is s-finite (#12591)
Added MeasureTheory.sFinite_withDensity_of_sigmaFinite_of_measurableView on Github →