mathlib3

9ef122d2 - feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590)

feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590) Various properties of `fin_meas_additive` and `dominated_fin_meas_additive` which will be useful to generalize results about integrals to `set_to_fun`.