α : Type u_1
β : Type ?u.149284
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure (μ + ν)) i = ↑(toENNRealVectorMeasure μ + toENNRealVectorMeasure ν) i
α : Type u_1
β : Type ?u.149284
m : MeasurableSpace α
μ ν : Measure α
⊢ toENNRealVectorMeasure (μ + ν) = toENNRealVectorMeasure μ + toENNRealVectorMeasure ν
refine' MeasureTheory.VectorMeasure.ext fun i hi => _
no goals
α : Type u_1
β : Type ?u.149284
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ ↑(toENNRealVectorMeasure (μ + ν)) i = ↑(toENNRealVectorMeasure μ + toENNRealVectorMeasure ν) i
rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
  toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]