∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_3} {μ : MeasureTheory.FiniteMeasure Ω} {T : Finset ι}
  {s : ι → Set Ω},
  (↑T).Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ι), MeasurableSet (s i)) → μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)