mathlib3

496a744e - feat(measure_theory): generalize `null_of_locally_null` to `outer_measure`, add versions (#11535)

feat(measure_theory): generalize `null_of_locally_null` to `outer_measure`, add versions (#11535) * generalize `null_of_locally_null`; * don't intersect with `s` twice; * add a contraposed version; * golf.