feat(measure_theory/measure_space): several lemmas about `restrict` (#3574)
feat(measure_theory/measure_space): several lemmas about `restrict` (#3574)





leanprover-community/mathlib,leanprover-community/mathlib