Commit 2021-09-18 23:07 6b96736f

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