∀ {α : Type u_1} {β : Type u_2} [mβ : MeasurableSpace β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ] (f : α → β), MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)