feat(measure_theory/measure/measure_space): The pushfoward measure of…

… a finite measure is a finite measure (#9186)

src/measure_theory/measure/measure_space.lean

@@ -1566,6 +1566,11 @@ lemma is_finite_measure_of_le (μ : measure α) [is_finite_measure μ] (h : ν 
   is_finite_measure ν :=
 { measure_univ_lt_top := lt_of_le_of_lt (h set.univ measurable_set.univ) (measure_lt_top _ _) }
 
+lemma measure.is_finite_measure_map {m : measurable_space α}
+  (μ : measure α) [is_finite_measure μ] {f : α → β} (hf : measurable f) :
+  is_finite_measure (map f μ) :=
+⟨by { rw map_apply hf measurable_set.univ, exact measure_lt_top μ _ }⟩
+
 @[simp] lemma measure_univ_nnreal_eq_zero [is_finite_measure μ] :
   measure_univ_nnreal μ = 0 ↔ μ = 0 :=
 begin