mathlib

eaa9e876 - chore(measure_theory/integral/set_to_l1): change definition of dominated_fin_meas_additive (#10585)

chore(measure_theory/integral/set_to_l1): change definition of dominated_fin_meas_additive (#10585) Change the definition to check the property only on measurable sets with finite measure (like every other property in that file). Also make some arguments of `set_to_fun` explicit to improve readability.