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"