Commit 2026-03-03 23:24 09e7054d

View on Github →

feat: countable intersections/unions of ae eq sets are ae eq (#36065) Also put some declarations in the Filter namespace so as to allow for dot notation.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

added theorem MeasureTheory.ae_eq_set_biInter

added theorem MeasureTheory.ae_eq_set_biUnion

Modified Mathlib/Order/Filter/CountableInter.lean

deleted theorem EventuallyEq.countable_bInter

deleted theorem EventuallyEq.countable_bUnion

deleted theorem EventuallyEq.countable_iInter

deleted theorem EventuallyEq.countable_iUnion

deleted theorem EventuallyLE.countable_bInter

deleted theorem EventuallyLE.countable_bUnion

deleted theorem EventuallyLE.countable_iInter

deleted theorem EventuallyLE.countable_iUnion

added theorem Filter.EventuallyEq.countable_bInter

added theorem Filter.EventuallyEq.countable_bUnion

added theorem Filter.EventuallyEq.countable_iInter

added theorem Filter.EventuallyEq.countable_iUnion

added theorem Filter.EventuallyLE.countable_bInter

added theorem Filter.EventuallyLE.countable_bUnion

added theorem Filter.EventuallyLE.countable_iInter

added theorem Filter.EventuallyLE.countable_iUnion

modified theorem Filter.mem_ofCountableInter

modified theorem Filter.mem_ofCountableUnion

modified def Filter.ofCountableInter

modified def Filter.ofCountableUnion

Modified Mathlib/Topology/Baire/BaireMeasurable.lean