# 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"