∀ {Ω : Type u_2} {Ω' : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) (f : Ω → Ω'), MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f ↑ν)