src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 66936 cf8d8fc23891
parent 65687 a68973661472
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -42,7 +42,7 @@
     1.4      have "(\<Sum>j<k + i. f j) = (\<Sum>j=i..<k + i. f j) + (\<Sum>j=0..<i. f j)"
     1.5        by (subst sum.union_disjoint[symmetric]) (auto intro!: sum.cong)
     1.6      also have "(\<Sum>j=i..<k + i. f j) = (\<Sum>j\<in>(\<lambda>n. n + i)`{0..<k}. f j)"
     1.7 -      unfolding image_add_atLeastLessThan by simp
     1.8 +      unfolding image_add_atLeast_lessThan by simp
     1.9      finally have "(\<Sum>j<k + i. f j) = (\<Sum>n<k. f (n + i)) + (\<Sum>j<i. f j)"
    1.10        by (auto simp: inj_on_def atLeast0LessThan sum.reindex) }
    1.11    ultimately have "(\<lambda>k. (\<Sum>n<k + i. f n)) \<longlonglongrightarrow> l + (\<Sum>j<i. f j)"