Commit 2023-02-09 14:33 a7589864

feat(measure_theory/integral/set_integral): remove or weaken some integrability assumptions (#18395) When dealing with integrals on sets, we assume almost always that the set is measurable or null-measurable. However, there are situations where these assumptions can be removed, making the lemmas easier to apply, but at the cost of more involved proofs. We implement this in this PR. As an example, we prove set_integral_eq_of_subset_of_forall_diff_eq_zero: if s is contained in t, and t is null-measurable and a function vanishes on t \ s, then its integrals on s and t coincide (no measurability assumptions on s or f). The special case t = univ is especially useful.