src/HOL/SEQ.thy
changeset 31588 2651f172c38b
parent 31488 5691ccb8d6b5
child 32064 53ca12ff305d
     1.1 --- a/src/HOL/SEQ.thy	Fri Jun 12 12:00:30 2009 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Fri Jun 12 15:46:21 2009 -0700
     1.3 @@ -348,23 +348,7 @@
     1.4    fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.5    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
     1.6    shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
     1.7 -proof (cases "finite S")
     1.8 -  case True
     1.9 -  thus ?thesis using n
    1.10 -  proof (induct)
    1.11 -    case empty
    1.12 -    show ?case
    1.13 -      by (simp add: LIMSEQ_const)
    1.14 -  next
    1.15 -    case insert
    1.16 -    thus ?case
    1.17 -      by (simp add: LIMSEQ_add)
    1.18 -  qed
    1.19 -next
    1.20 -  case False
    1.21 -  thus ?thesis
    1.22 -    by (simp add: LIMSEQ_const)
    1.23 -qed
    1.24 +using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
    1.25  
    1.26  lemma LIMSEQ_setprod:
    1.27    fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"