# HG changeset patch
# User hoelzl
# Date 1349863942 -7200
# Node ID d5c6a905b57e5391bd242cf082a0ede5cb011f98
# Parent  59b219ca3513fc4b107bd36dbe45eed49e667c60
add measurable_compose

diff -r 59b219ca3513 -r d5c6a905b57e src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:21 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:22 2012 +0200
@@ -1310,6 +1310,10 @@
   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"