Removed unnecessary assumption
authorhoelzl
Tue May 04 17:53:20 2010 +0200 (2010-05-04)
changeset 36647edc381bf7200
parent 36646 8687bc6608d6
child 36648 43b66dcd9266
Removed unnecessary assumption
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/SEQ.thy	Tue May 04 16:25:16 2010 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Tue May 04 17:53:20 2010 +0200
     1.3 @@ -544,10 +544,12 @@
     1.4  
     1.5  lemma convergent_setsum:
     1.6    fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
     1.7 -  assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
     1.8 +  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
     1.9    shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
    1.10 -using assms
    1.11 -by (induct A set: finite, simp_all add: convergent_const convergent_add)
    1.12 +proof (cases "finite A")
    1.13 +  case True with assms show ?thesis
    1.14 +    by (induct A set: finite) (simp_all add: convergent_const convergent_add)
    1.15 +qed (simp add: convergent_const)
    1.16  
    1.17  lemma (in bounded_linear) convergent:
    1.18    assumes "convergent (\<lambda>n. X n)"