mathlib3

e3eb0eb0 - feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)