src/HOL/Probability/Measurable.thy
 changeset 57025 e7fd64f82876 parent 56993 e5366291d6aa child 58965 a62cdcc5344b
```     1.1 --- a/src/HOL/Probability/Measurable.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Probability/Measurable.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -330,6 +330,31 @@
1.4    "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
1.5    by simp
1.6
1.7 +lemma measurable_card[measurable]:
1.8 +  fixes S :: "'a \<Rightarrow> nat set"
1.9 +  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
1.10 +  shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)"
1.11 +  unfolding measurable_count_space_eq2_countable
1.12 +proof safe
1.13 +  fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M"
1.14 +  proof (cases n)
1.15 +    case 0
1.16 +    then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = {x\<in>space M. infinite (S x) \<or> (\<forall>i. i \<notin> S x)}"
1.17 +      by auto
1.18 +    also have "\<dots> \<in> sets M"
1.19 +      by measurable
1.20 +    finally show ?thesis .
1.21 +  next
1.22 +    case (Suc i)
1.23 +    then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
1.24 +      (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
1.25 +      unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
1.26 +    also have "\<dots> \<in> sets M"
1.27 +      by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
1.28 +    finally show ?thesis .
1.29 +  qed
1.30 +qed rule
1.31 +
1.32  subsection {* Measurability for (co)inductive predicates *}
1.33
1.34  lemma measurable_lfp:
```