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)