Mathlib Changelog
v4
Changelog
About
Github
Theorem
aestronglyMeasurable_indicator_iff₀
Modification history
2025-11-04 09:42
Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
feat: indicator of a null measurable set is aestronglymeasurable (#31158)
Added
aestronglyMeasurable_indicator_iff₀
View on Github →