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