mathlib3

a5d2dbc5 - chore(measure_theory/integral/set_integral): generalize, golf (#9328)

chore(measure_theory/integral/set_integral): generalize, golf (#9328) * rename `integrable_on_finite_union` to `integrable_on_finite_Union`; * rename `integrable_on_finset_union` to `integrable_on_finset_Union`; * add `integrable_on_fintype_Union`; * generalize `tendsto_measure_Union` and `tendsto_measure_Inter from `s : ℕ → set α` to `[semilattice_sup ι] [encodable ι] {s : ι → set α}`; * add `integral_diff`; * generalize `integral_finset_bUnion`, `integral_fintype_Union` and `has_sum_integral_Union` to require appropriate `integrable_on` instead of `integrable`; * golf some proofs.