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