# HG changeset patch
# User nipkow
# Date 1101220331 -3600
# Node ID 7d6e12ead9648a43ef956baec3a828bf53a19e40
# Parent  2ca1c66a6758ab78df45c1cfd32c24c21e066cc7
added lemma

diff -r 2ca1c66a6758 -r 7d6e12ead964 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Tue Nov 23 15:25:39 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Tue Nov 23 15:32:11 2004 +0100
@@ -277,6 +277,27 @@
 lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
 
+lemma LIMSEQ_setsum:
+  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
+  shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
+proof (cases "finite S")
+  case True
+  thus ?thesis using n
+  proof (induct)
+    case empty
+    show ?case
+      by (simp add: LIMSEQ_const)
+  next
+    case insert
+    thus ?case
+      by (simp add: LIMSEQ_add)
+  qed
+next
+  case False
+  thus ?thesis
+    by (simp add: setsum_def LIMSEQ_const)
+qed
+
 
 subsection{*Nslim and Lim*}