src/HOL/Probability/Sigma_Algebra.thy
changeset 57137 f174712d0a84
parent 57025 e7fd64f82876
child 57138 7b3146180291
     1.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 18:13:40 2014 +0200
     1.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri May 30 15:56:30 2014 +0200
     1.3 @@ -2351,9 +2351,9 @@
     1.4  qed
     1.5  
     1.6  lemma measurable_restrict_space2:
     1.7 -  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     1.8 +  "\<Omega> \<inter> space N \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
     1.9      f \<in> measurable M (restrict_space N \<Omega>)"
    1.10 -  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
    1.11 +  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric])
    1.12  
    1.13  end
    1.14