src/HOL/Probability/Infinite_Product_Measure.thy
changeset 43679 052eaf7509cf
parent 42950 6e5c2a3c69da
child 43920 cedb5cb948fd
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jul 05 19:11:29 2011 +0200
     1.3 @@ -844,7 +844,7 @@
     1.4      by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
     1.5  qed
     1.6  
     1.7 -lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A"
     1.8 +lemma sigma_sets_superset_generator: "A \<subseteq> sigma_sets X A"
     1.9    by (auto intro: sigma_sets.Basic)
    1.10  
    1.11  lemma (in product_prob_space) infprod_algebra_alt:
    1.12 @@ -859,7 +859,7 @@
    1.13      fix J assume J: "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
    1.14      have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
    1.15      also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
    1.16 -    also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq)
    1.17 +    also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_superset_generator)
    1.18      finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> sigma_sets ?O ?G" .
    1.19      have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
    1.20        by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)