src/HOL/Series.thy
changeset 63952 354808e9f44b
parent 63680 6e1e8b5abbfa
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Series.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Series.thy	Wed Sep 28 17:01:01 2016 +0100
     1.3 @@ -26,12 +26,16 @@
     1.4      (binder "\<Sum>" 10)
     1.5    where "suminf f = (THE s. f sums s)"
     1.6  
     1.7 +text\<open>Variants of the definition\<close>
     1.8  lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
     1.9    apply (simp add: sums_def)
    1.10    apply (subst LIMSEQ_Suc_iff [symmetric])
    1.11    apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
    1.12    done
    1.13  
    1.14 +lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
    1.15 +  by (simp add: sums_def' atMost_atLeast0)
    1.16 +
    1.17  
    1.18  subsection \<open>Infinite summability on topological monoids\<close>
    1.19