Equivalent theorems for lebesgue integral from Bochner

Stream: Is there code for X?

[Pietro Lavino]

I proved some result using the Bochner integral, and realized just now it might be more convenient to have with the lebesgue integral instead. several lemmas and mathlib theorem were necessary and was wondering if equivalent theorems were available for the lebesgue integral of the following, `setIntegral_congr_ae₀, setIntegral_const,integral_iUnion_ae '. Is there any theorems relating the bochner and lebesgue integral, perhaps they are equivalent in certain cases?

[Yury G. Kudryashov]

@loogle MeasureTheory.integral, MeasureTheory.lintegral

[loogle]

:search: MeasureTheory.lintegral_coe_eq_integral, MeasureTheory.norm_integral_le_lintegral_norm, and 27 more