--- a/src/HOL/Library/Indicator_Function.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Mon Jun 30 15:45:21 2014 +0200
@@ -142,4 +142,17 @@
"A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
by (auto split: split_indicator simp: fun_eq_iff)
+lemma indicator_sums:
+ assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
+ shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
+proof cases
+ assume "\<exists>i. x \<in> A i"
+ then obtain i where i: "x \<in> A i" ..
+ with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
+ by (intro sums_finite) (auto split: split_indicator)
+ also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
+ using i by (auto split: split_indicator)
+ finally show ?thesis .
+qed simp
+
end