mathlib

f4991b97 - feat(measure_theory/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) (#7918)