∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [T2Space M] {v : MeasureTheory.VectorMeasure α M} {A : Set α}, MeasurableSet A → ↑v Aᶜ = ↑v Set.univ - ↑v A