src/HOL/Probability/Infinite_Product_Measure.thy
changeset 50095 94d7dfa9f404
parent 50087 635d73673b5e
child 50099 a58bb401af80
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 11:22:22 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 16 11:34:34 2012 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4          using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
     1.5        ultimately have "0 < ?a" by auto
     1.6  
     1.7 -      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (PiP J M (\<lambda>J. (Pi\<^isub>M J M))) X"
     1.8 +      have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (limP J M (\<lambda>J. (Pi\<^isub>M J M))) X"
     1.9          using A by (intro allI generator_Ex) auto
    1.10        then obtain J' X' where J': "\<And>n. J' n \<noteq> {}" "\<And>n. finite (J' n)" "\<And>n. J' n \<subseteq> I" "\<And>n. X' n \<in> sets (Pi\<^isub>M (J' n) M)"
    1.11          and A': "\<And>n. A n = emb I (J' n) (X' n)"