--- a/src/HOL/Library/Indicator_Function.thy Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Fri Nov 14 13:18:33 2014 +0100
@@ -57,6 +57,9 @@
lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
unfolding indicator_def by (cases x) auto
+lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
+ by (auto simp: indicator_def inj_on_def)
+
lemma
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"