src/HOL/Probability/Projective_Family.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -641,7 +641,7 @@
     1.4        proof (subst distr_distr)
     1.5          have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M UNIV (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x i
     1.6            using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
     1.7 -        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (UNION UNIV J) M)"
     1.8 +        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (\<Union>(J ` UNIV)) M)"
     1.9            by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
    1.10        qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
    1.11        also have "\<dots> = distr (distr IT.PF.lim (PiM (t`J i) (\<lambda>x. M (f x))) (\<lambda>\<omega>. restrict \<omega> (t`J i))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"