--- a/src/HOL/Series.thy Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Series.thy Wed Sep 28 17:01:01 2016 +0100
@@ -26,12 +26,16 @@
(binder "\<Sum>" 10)
where "suminf f = (THE s. f sums s)"
+text\<open>Variants of the definition\<close>
lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
apply (simp add: sums_def)
apply (subst LIMSEQ_Suc_iff [symmetric])
apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
done
+lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
+ by (simp add: sums_def' atMost_atLeast0)
+
subsection \<open>Infinite summability on topological monoids\<close>