src/HOL/Series.thy
 changeset 63040 eb4ddd18d635 parent 62381 a6479cb85944 child 63145 703edebd1d92
```     1.1 --- a/src/HOL/Series.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/Series.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -84,7 +84,7 @@
1.4    shows   "summable f = summable g"
1.5  proof -
1.6    from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder)
1.7 -  def C \<equiv> "(\<Sum>k<N. f k - g k)"
1.8 +  define C where "C = (\<Sum>k<N. f k - g k)"
1.9    from eventually_ge_at_top[of N]
1.10      have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
1.11    proof eventually_elim
1.12 @@ -1048,7 +1048,7 @@
1.13    finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" .
1.14  next
1.15    assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c"
1.16 -  def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n"
1.17 +  define g_inv where "g_inv n = (LEAST m. g m \<ge> n)" for n
1.18    from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
1.19      by (auto simp: filterlim_at_top eventually_at_top_linorder)
1.20    hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex)
```