# HG changeset patch
# User Andreas Lochbihler
# Date 1416569099 -3600
# Node ID 5fcfeae84b963317b07206ec83b66d8181221cd7
# Parent  4999a616336c420c7afc139f2991c26221d576df
add lemma

diff -r 4999a616336c -r 5fcfeae84b96 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 21 12:11:44 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 21 12:24:59 2014 +0100
@@ -603,6 +603,12 @@
     by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
 qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
 
+lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
+apply(simp add: set_eq_iff set_pmf_iff pmf_join)
+apply(subst integral_nonneg_eq_0_iff_AE)
+apply(auto simp add: pmf_le_1 pmf_nonneg AE_measure_pmf_iff intro!: measure_pmf.integrable_const_bound[where B=1])
+done
+
 lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
   by (auto intro!: prob_space_return simp: AE_return measure_return)