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 →