Commit 2021-09-22 12:11 a5d2dbc5

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.