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