mathlib3
4e313969 - feat(measure_theory/measure): define `ae_disjoint` (#11500)

Commit

3 years ago

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

Author

urkud

Parents