∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} {μ : MeasureTheory.VectorMeasure α ENNReal},
  (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → ↑v s = 0) ↔ v.AbsolutelyContinuous μ