Commit 2023-05-06 06:40 9831a01e

View on Github →

feat: port MeasureTheory.Measure.AEDisjoint (#3351)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/AEDisjoint.lean

added theorem MeasureTheory.AEDisjoint.diff_ae_eq_left

added theorem MeasureTheory.AEDisjoint.diff_ae_eq_right

added theorem MeasureTheory.AEDisjoint.exists_disjoint_diff

added theorem MeasureTheory.AEDisjoint.measure_diff_left

added theorem MeasureTheory.AEDisjoint.measure_diff_right

added theorem MeasureTheory.AEDisjoint.mono_ae

added theorem MeasureTheory.AEDisjoint.of_null_left

added theorem MeasureTheory.AEDisjoint.of_null_right

added theorem MeasureTheory.AEDisjoint.union_left

added theorem MeasureTheory.AEDisjoint.union_left_iff

added theorem MeasureTheory.AEDisjoint.union_right

added theorem MeasureTheory.AEDisjoint.union_right_iff

added theorem MeasureTheory.AEDisjoint.unionᵢ_left_iff

added theorem MeasureTheory.AEDisjoint.unionᵢ_right_iff

added def MeasureTheory.AEDisjoint

added theorem MeasureTheory.aedisjoint_compl_left

added theorem MeasureTheory.aedisjoint_compl_right

added theorem MeasureTheory.exists_null_pairwise_disjoint_diff