equal
deleted
inserted
replaced
94 assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0") |
94 assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0") |
95 moreover have "0 \<le> ?a" |
95 moreover have "0 \<le> ?a" |
96 using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) |
96 using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def) |
97 ultimately have "0 < ?a" by auto |
97 ultimately have "0 < ?a" by auto |
98 |
98 |
99 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" |
99 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" |
100 using A by (intro allI generator_Ex) auto |
100 using A by (intro allI generator_Ex) auto |
101 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)" |
101 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)" |
102 and A': "\<And>n. A n = emb I (J' n) (X' n)" |
102 and A': "\<And>n. A n = emb I (J' n) (X' n)" |
103 unfolding choice_iff by blast |
103 unfolding choice_iff by blast |
104 moreover def J \<equiv> "\<lambda>n. (\<Union>i\<le>n. J' i)" |
104 moreover def J \<equiv> "\<lambda>n. (\<Union>i\<le>n. J' i)" |