integral Union

Stream: Is there code for X?

[Jason KY.]

Do we have something like this?

import measure_theory.integral.set_integral

variables {α E : Type*} {m : measurable_space α}

open measure_theory topological_space

variables [normed_group E] [measurable_space E] {f : α → E} [borel_space E]
  [second_countable_topology E] [complete_space E] [normed_space ℝ E] {μ : measure α}

lemma integral_Union {f : α → E} {s : ℕ → set α}
  (hf : integrable f μ) (hs₁ : pairwise (disjoint on s)) (hs₂ : ∀ n, measurable_set (s n)) :
  has_sum (λ n, ∫ x in s n, f x ∂μ) (∫ x in ⋃ n, s n, f x ∂μ) :=
begin
  sorry
end

If not, is there an easy way of proving this? I'm not very familiar with proving statements about Bochner integrals. Thanks!