Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-04 09:42
3b8deacd
View on Github →
feat: indicator of a null measurable set is aestronglymeasurable (
#31158
)
Estimated changes
Modified
Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
added
theorem
aestronglyMeasurable_indicator_iff₀