Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-05-07 10:24
aa797706
View on Github →
feat:
withDensity
of an s-finite measure is s-finite (
#12591
)
Estimated changes
Modified
Mathlib/MeasureTheory/Measure/WithDensity.lean
added
theorem
MeasureTheory.sFinite_withDensity_of_measurable
added
theorem
MeasureTheory.sFinite_withDensity_of_sigmaFinite_of_measurable