src/HOL/Probability/Sigma_Algebra.thy

   apply (auto simp add: measurable_def vimage_compose)
   apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
   apply force+
   done
 
+lemma measurable_compose:
+  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
+  using measurable_comp[of f M N g L] by (simp add: comp_def)
+
 lemma measurable_Least:
   assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
   shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
 proof -
   { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"