∀ {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α)
  (μ : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.AbsolutelyContinuous c μ ↔
    MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.re c) μ ∧
      MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.im c) μ