Commit 2022-01-18 09:14 a217b9c3

feat(measure_theory): drop some measurable_set assumptions (#11536)

• make exists_subordinate_pairwise_disjoint work for null_measurable_sets;
• use ae_disjoint in measure_Union₀, drop measure_Union_of_null_inter;
• prove measure_inter_add_diff for null_measurable_sets;
• drop some measurable_set assumptions in measure_union, measure_diff, etc;
• golf.