Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 15:10 4e313969

View on Github →

feat(measure_theory/measure): define ae_disjoint (#11500) I am going to migrate most disjoint assumptions to ae_disjoint.

Estimated changes

Created src/measure_theory/measure/ae_disjoint.lean

added theorem disjoint.ae_disjoint

added theorem measure_theory.ae_disjoint.Union_left_iff

added theorem measure_theory.ae_disjoint.Union_right_iff

added theorem measure_theory.ae_disjoint.exists_disjoint_diff

added theorem measure_theory.ae_disjoint.mono

added theorem measure_theory.ae_disjoint.mono_ae

added theorem measure_theory.ae_disjoint.of_null_left

added theorem measure_theory.ae_disjoint.of_null_right

added theorem measure_theory.ae_disjoint.union_left

added theorem measure_theory.ae_disjoint.union_left_iff

added theorem measure_theory.ae_disjoint.union_right

added theorem measure_theory.ae_disjoint.union_right_iff

added def measure_theory.ae_disjoint

added theorem measure_theory.exists_null_pairwise_disjoint_diff

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.measure_mono_null_ae