Commit 2021-12-07 21:13 eaa9e876
View on Github →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.