Commit 2023-05-21 15:13 d3369c5b

View on Github →

feat: port MeasureTheory.Function.AEMeasurableOrder (#4073)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

added theorem ENNReal.aemeasurable_of_exist_almost_disjoint_supersets

added theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets