src/HOL/Probability/Sigma_Algebra.thy

   have "{x\<in>\<Omega>. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>\<Omega>. P i x})" by auto
   with assms show ?thesis by auto
 qed
 
 lemma (in sigma_algebra) sets_Collect_countable_Ex':
-  assumes "\<And>i. {x\<in>\<Omega>. P i x} \<in> M"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
   assumes "countable I"
   shows "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} \<in> M"
 proof -
   have "{x\<in>\<Omega>. \<exists>i\<in>I. P i x} = (\<Union>i\<in>I. {x\<in>\<Omega>. P i x})" by auto
   with assms show ?thesis 
     by (auto intro!: countable_UN')
+qed
+
+lemma (in sigma_algebra) sets_Collect_countable_All':
+  assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
+  assumes "countable I"
+  shows "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} \<in> M"
+proof -
+  have "{x\<in>\<Omega>. \<forall>i\<in>I. P i x} = (\<Inter>i\<in>I. {x\<in>\<Omega>. P i x}) \<inter> \<Omega>" by auto
+  with assms show ?thesis 
+    by (cases "I = {}") (auto intro!: countable_INT')
+qed
+
+lemma (in sigma_algebra) sets_Collect_countable_Ex1':
+  assumes "\<And>i. i \<in> I \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M"
+  assumes "countable I"
+  shows "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} \<in> M"
+proof -
+  have "{x\<in>\<Omega>. \<exists>!i\<in>I. P i x} = {x\<in>\<Omega>. \<exists>i\<in>I. P i x \<and> (\<forall>j\<in>I. P j x \<longrightarrow> i = j)}"
+    by auto
+  with assms show ?thesis 
+    by (auto intro!: sets_Collect_countable_All' sets_Collect_countable_Ex' sets_Collect_conj sets_Collect_imp sets_Collect_const)
 qed
 
 lemmas (in sigma_algebra) sets_Collect =
   sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const
   sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All

 lemma measurable_compose_rev:
   assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
   shows "(\<lambda>x. f (g x)) \<in> measurable M N"
   using measurable_compose[OF g f] .
 
+lemma measurable_count_space_eq_countable:
+  assumes "countable A"
+  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+    with `countable A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "countable X"
+      by (auto dest: countable_subset)
+    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
+    ultimately have "f -` X \<inter> space M \<in> sets M"
+      using `X \<subseteq> A` by (auto intro!: sets.countable_UN' simp del: UN_simps) }
+  then show ?thesis
+    unfolding measurable_def by auto
+qed
 
 subsection {* Extend measure *}
 
 definition "extend_measure \<Omega> I G \<mu> =
   (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)

   by (auto simp: subset_eq)
 
 subsection {* Sigma algebra generated by function preimages *}
 
 definition
-  "vimage_algebra M S f = sigma S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
+  "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
 
 lemma sigma_algebra_preimages:
   fixes f :: "'x \<Rightarrow> 'a"
   assumes "f \<in> S \<rightarrow> space M"
   shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)"