src/HOL/Probability/Projective_Family.thy
changeset 57418 6ab1c7cb0b8d
parent 53015 a1119cf551e8
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4      by simp
     1.5    also have "\<dots> = (\<Prod> i\<in>K. emeasure (M i) (if i \<in> J then E i else space (M i)))"
     1.6      using `finite K` `J \<subseteq> K`
     1.7 -    by (intro setprod_mono_one_left) (auto simp: M.emeasure_space_1)
     1.8 +    by (intro setprod.mono_neutral_left) (auto simp: M.emeasure_space_1)
     1.9    also have "\<dots> = emeasure (Pi\<^sub>M K M) (\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i))"
    1.10      using E by (simp add: K.measure_times)
    1.11    also have "(\<Pi>\<^sub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^sub>E J E \<inter> (\<Pi>\<^sub>E i\<in>K. space (M i))"