∀ {α : Type u_1} {m : MeasurableSpace α} {L : Type u_3} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid L]
  [inst_1 : TopologicalSpace L] [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : TopologicalSpace N] {u : MeasureTheory.VectorMeasure α L} {v : MeasureTheory.VectorMeasure α M}
  {w : MeasureTheory.VectorMeasure α N}, u.AbsolutelyContinuous v → v.AbsolutelyContinuous w → u.AbsolutelyContinuous w