mathlib3

0d09e993 - feat(measure_theory/integral/{set_to_l1,bochner}): generalize results about integrals to `set_to_fun` (#10369)

feat(measure_theory/integral/{set_to_l1,bochner}): generalize results about integrals to `set_to_fun` (#10369) The Bochner integral is a particular case of the `set_to_fun` construction. We generalize some lemmas which were proved for integrals to `set_to_fun`, notably the Lebesgue dominated convergence theorem.