mathlib3

6dd65257 - feat(measure_theory/measure/measure_space): better definition of to_measurable (#11529)

feat(measure_theory/measure/measure_space): better definition of to_measurable (#11529) Currently, `to_measurable μ t` picks a measurable superset of `t` with the same measure. When the measure of `t` is infinite, it is most often useless. This PR adjusts the definition so that, in the case of sigma-finite spaces, `to_measurable μ t` has good properties even when `t` has infinite measure.