feat(measure_theory/measure/measure_space_def): some simple lemmas about measures and intersection (#9306)
feat(measure_theory/measure/measure_space_def): some simple lemmas about measures and intersection (#9306)

From #2819 






leanprover-community/mathlib,leanprover-community/mathlib