Commit 2024-06-08 17:32 b65219f6

feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. (#10856) add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in MeasureTheory/Measure/NullMeasurable.lean to be an instance of this general construction. The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition. TODO: Similarly generalize things about AEMeasurable, where appropriate.