src/HOL/Series.thy
changeset 46904 f30e941b4512
parent 44727 d45acd50a894
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Series.thy	Tue Mar 13 16:22:18 2012 +0100
     1.2 +++ b/src/HOL/Series.thy	Tue Mar 13 16:40:06 2012 +0100
     1.3 @@ -87,10 +87,13 @@
     1.4    by (simp add: sums_def summable_def, blast)
     1.5  
     1.6  lemma summable_sums:
     1.7 -  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" assumes "summable f" shows "f sums (suminf f)"
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
     1.9 +  assumes "summable f"
    1.10 +  shows "f sums (suminf f)"
    1.11  proof -
    1.12 -  from assms guess s unfolding summable_def sums_def_raw .. note s = this
    1.13 -  then show ?thesis unfolding sums_def_raw suminf_def
    1.14 +  from assms obtain s where s: "(\<lambda>n. setsum f {0..<n}) ----> s"
    1.15 +    unfolding summable_def sums_def [abs_def] ..
    1.16 +  then show ?thesis unfolding sums_def [abs_def] suminf_def
    1.17      by (rule theI, auto intro!: tendsto_unique[OF trivial_limit_sequentially])
    1.18  qed
    1.19