Commit 2026-08-20 12:42 e2d64cff

chore: split too long file Measure.MeasureSpace (#42949) Split Measure.MeasureSpace into 8 files:

• Basic contains all the lemmas related to operations on sets;
• Continuity contains lemmas related to continuity from above and below;
• OuterMeasure defines OuterMeasure.toMeasure;
• Module provides the Module instance on measures;
• CompleteLattice provides the CompleteLattice instance on measures;
• Sum defines Measure.sum;
• Filter proves properties about ae that require Module or CompleteLattice and define cofinite;
• Interval provides lemmas related to intervals in general preorders. Also remove the names of some instances and move MeasureTheory.ae_uIoc_iff next to MeasureTheory.ae_restrict_uIoc_iff.