∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : ContinuousAdd M] (v w : MeasureTheory.VectorMeasure α M) (i : Set α), ↑(v + w) i = ↑v i + ↑w i