src/HOL/Probability/Independent_Family.thy
changeset 56154 f0a927235162
parent 55414 eab03e9cee8a
child 57235 b0b9a10e4bf4
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -794,10 +794,10 @@
     1.4      { fix A assume "A \<in> sets (N i)"
     1.5        then have "\<exists>B. (Y i \<circ> X i) -` A \<inter> space M = X i -` B \<inter> space M \<and> B \<in> sets (M' i)"
     1.6          by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
     1.7 -           (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
     1.8 +           (auto simp: vimage_comp intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
     1.9      then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
    1.10        sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
    1.11 -      by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
    1.12 +      by (intro sigma_sets_subseteq) (auto simp: vimage_comp)
    1.13    qed
    1.14  qed
    1.15