equal
deleted
inserted
replaced
54 lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)" |
54 lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)" |
55 unfolding indicator_def by (cases x) auto |
55 unfolding indicator_def by (cases x) auto |
56 |
56 |
57 lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)" |
57 lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)" |
58 unfolding indicator_def by (cases x) auto |
58 unfolding indicator_def by (cases x) auto |
|
59 |
|
60 lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)" |
|
61 by (auto simp: indicator_def inj_on_def) |
59 |
62 |
60 lemma |
63 lemma |
61 fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A" |
64 fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A" |
62 shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
65 shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)" |
63 and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |
66 and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)" |