no goals
α : Type u_2
ι : Type u_1
m : ι → OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ ↑(sum m) t = ↑(sum m) (t ∩ s) + ↑(sum m) (t \ s)
simp [fun i => MeasurableSpace.measurableSet_iInf.1 h i t, ENNReal.tsum_add]