| changeset 22942 | bf718970e5ef |
| parent 22912 | c477862c566d |
| child 22972 | 3e96b98d37c6 |
--- a/src/HOL/Real/RealVector.thy Fri May 11 20:47:30 2007 +0200 +++ b/src/HOL/Real/RealVector.thy Sat May 12 18:16:30 2007 +0200 @@ -32,6 +32,14 @@ lemma (in additive) diff: "f (x - y) = f x - f y" by (simp add: diff_def add minus) +lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))" +apply (cases "finite A") +apply (induct set: finite) +apply (simp add: zero) +apply (simp add: add) +apply (simp add: zero) +done + subsection {* Real vector spaces *}