src/HOL/Probability/Probability_Mass_Function.thy
 changeset 69313 b021008c5397 parent 68386 98cf1c823c48 child 69529 4ab9657b3257
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -1851,15 +1851,15 @@
1.4    uniformly at random.
1.5  \<close>
1.6  lemma pmf_of_set_UN:
1.7 -  assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
1.8 +  assumes "finite (\<Union>(f ` A))" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
1.9            "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A"
1.10 -  shows   "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
1.11 +  shows   "pmf_of_set (\<Union>(f ` A)) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
1.12              (is "?lhs = ?rhs")
1.13  proof (intro pmf_eqI)
1.14    fix x
1.15    from assms have [simp]: "finite A"
1.16      using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast
1.17 -  from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) =
1.18 +  from assms have "ereal (pmf (pmf_of_set (\<Union>(f ` A))) x) =
1.19      ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))"
1.20      by (subst pmf_of_set) auto
1.21    also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
```