{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        {f : Ω → Ω'} → Measurable f → MeasureTheory.FiniteMeasure Ω →ₗ[NNReal] MeasureTheory.FiniteMeasure Ω'