author hoelzl Mon, 13 Jul 2015 14:40:16 +0200 changeset 60715 ee0afee54b1d parent 60714 ff8aa76d6d1c child 60716 8e82a83757df
```--- 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)

+  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 =```