mathlib

6b96736f - feat(measure_theory/integral/set_to_L1): image of an indicator by set_to_fun (and related functions) (#9205)

feat(measure_theory/integral/set_to_L1): image of an indicator by set_to_fun (and related functions) (#9205) We show the following equality, as well as versions of it for other intermediate `set_to_*` functions: ``` set_to_fun (hT : dominated_fin_meas_additive μ T C) (s.indicator (λ _, x)) = T s x ```