src/HOL/Limits.thy
changeset 31588 2651f172c38b
parent 31565 da5a5589418e
child 31902 862ae16a799d
     1.1 --- a/src/HOL/Limits.thy	Fri Jun 12 12:00:30 2009 -0700
     1.2 +++ b/src/HOL/Limits.thy	Fri Jun 12 15:46:21 2009 -0700
     1.3 @@ -471,6 +471,24 @@
     1.4    shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
     1.5  by (simp add: diff_minus tendsto_add tendsto_minus)
     1.6  
     1.7 +lemma tendsto_setsum [tendsto_intros]:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
     1.9 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net"
    1.10 +  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net"
    1.11 +proof (cases "finite S")
    1.12 +  assume "finite S" thus ?thesis using assms
    1.13 +  proof (induct set: finite)
    1.14 +    case empty show ?case
    1.15 +      by (simp add: tendsto_const)
    1.16 +  next
    1.17 +    case (insert i F) thus ?case
    1.18 +      by (simp add: tendsto_add)
    1.19 +  qed
    1.20 +next
    1.21 +  assume "\<not> finite S" thus ?thesis
    1.22 +    by (simp add: tendsto_const)
    1.23 +qed
    1.24 +
    1.25  lemma (in bounded_linear) tendsto [tendsto_intros]:
    1.26    "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
    1.27  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)