src/HOL/Hyperreal/Series.thy
changeset 20689 4950e45442b8
parent 20688 690d866a165d
child 20692 6df83a636e67
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 03:38:36 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 04:00:03 2006 +0200
     1.3 @@ -337,6 +337,16 @@
     1.4   "summable f = convergent (%n. setsum f {0..<n})"
     1.5  by (simp add: summable_def sums_def convergent_def)
     1.6  
     1.7 +lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
     1.8 +apply (drule summable_convergent_sumr_iff [THEN iffD1])
     1.9 +apply (drule Cauchy_convergent_iff [THEN iffD2])
    1.10 +apply (simp only: Cauchy_def LIMSEQ_def, safe)
    1.11 +apply (drule_tac x="r" in spec, safe)
    1.12 +apply (rule_tac x="M" in exI, safe)
    1.13 +apply (drule_tac x="Suc n" in spec, simp)
    1.14 +apply (drule_tac x="n" in spec, simp)
    1.15 +done
    1.16 +
    1.17  lemma summable_Cauchy:
    1.18       "summable f =  
    1.19        (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"