# HG changeset patch
# User hoelzl
# Date 1436791216 -7200
# Node ID ee0afee54b1d9f728342d2eed25a70595bda37f3
# Parent  ff8aa76d6d1c7d62bcaa9987147cea0f05f0dcff
add emeasure_add_AE

diff -r ff8aa76d6d1c -r ee0afee54b1d src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Mon Jul 13 14:39:50 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Mon Jul 13 14:40:16 2015 +0200
@@ -1112,6 +1112,21 @@
   using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"]
   by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets)
 
+lemma emeasure_add_AE:
+  assumes [measurable]: "A \<in> sets M" "B \<in> sets M" "C \<in> sets M"
+  assumes 1: "AE x in M. x \<in> C \<longleftrightarrow> x \<in> A \<or> x \<in> B"
+  assumes 2: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)"
+  shows "emeasure M C = emeasure M A + emeasure M B"
+proof -
+  have "emeasure M C = emeasure M (A \<union> B)"
+    by (rule emeasure_eq_AE) (insert 1, auto)
+  also have "\<dots> = emeasure M A + emeasure M (B - A)"
+    by (subst plus_emeasure) auto
+  also have "emeasure M (B - A) = emeasure M B"
+    by (rule emeasure_eq_AE) (insert 2, auto)
+  finally show ?thesis .
+qed
+
 subsection {* @{text \<sigma>}-finite Measures *}
 
 locale sigma_finite_measure =