src/HOL/Probability/Probability_Mass_Function.thy
changeset 59496 6faf024a1893
parent 59495 03944a830c4a
parent 59492 ef195926dd98
child 59525 dfe6449aecd8
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 13:50:30 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 14:06:57 2015 +0100
     1.3 @@ -282,6 +282,9 @@
     1.4      using measure_pmf.emeasure_space_1 by simp
     1.5  qed
     1.6  
     1.7 +lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
     1.8 +using measure_pmf.emeasure_space_1[of M] by simp
     1.9 +
    1.10  lemma in_null_sets_measure_pmfI:
    1.11    "A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
    1.12  using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]