Commit 2021-06-09 15:40 d0ed2a42

chore(measure_theory/set_integral): put the definition of integrable_on into a new file (#7842) The file measure_theory.set_integral is split into two: the integrable_on predicate is put into its own file, which does not import measure_theory.bochner_integration (this puts the definition of that integrability property before the definition of the actual integral). The file measure_theory.set_integral retains all facts about set_integral.