src/HOL/Probability/Infinite_Product_Measure.thy
changeset 50040 5da32dc55cd8
parent 50039 bfd5198cbe40
child 50041 afe886a04198
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 07 11:33:27 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 07 14:41:49 2012 +0100
     1.3 @@ -87,6 +87,11 @@
     1.4    fix J::"'i set" assume "finite J"
     1.5    interpret f: finite_product_prob_space M J proof qed fact
     1.6    show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) \<noteq> \<infinity>" by simp
     1.7 +  show "\<exists>A. range A \<subseteq> sets (Pi\<^isub>M J M) \<and>
     1.8 +            (\<Union>i. A i) = space (Pi\<^isub>M J M) \<and>
     1.9 +            (\<forall>i. emeasure (Pi\<^isub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
    1.10 +    by (auto simp add: sigma_finite_measure_def)
    1.11 +  show "emeasure (Pi\<^isub>M J M) (space (Pi\<^isub>M J M)) = 1" by (rule f.emeasure_space_1)
    1.12  qed simp_all
    1.13  
    1.14  lemma (in projective_family) prod_emb_injective: