Commit 2026-10-21 09:23 b575e0bb

View on Github →

chore: generalize lemmas about measurability of biUnion (#45097) Zulip discussion at #mathlib4 > Set is a one-field structure @ 💬

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

modified theorem MeasurableSet.biInter

modified theorem Set.Finite.measurableSet_biInter

modified theorem Set.Finite.measurableSet_biUnion

Modified Mathlib/MeasureTheory/Measure/Continuity.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

modified theorem Set.Finite.nullMeasurableSet_biInter

modified theorem Set.Finite.nullMeasurableSet_biUnion

Modified Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean

Modified Mathlib/Probability/Process/Stopping.lean