src/HOL/Series.thy
changeset 59613 7103019278f0
parent 59025 d885cff91200
child 59712 6c013328b885
     1.1 --- a/src/HOL/Series.thy	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/HOL/Series.thy	Thu Mar 05 17:30:29 2015 +0000
     1.3 @@ -125,6 +125,11 @@
     1.4  lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
     1.5    by (metis summable_sums sums_summable sums_unique)
     1.6  
     1.7 +lemma sums_unique2:
     1.8 +  fixes a b :: "'a::{comm_monoid_add,t2_space}"
     1.9 +  shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
    1.10 +by (simp add: sums_iff)
    1.11 +
    1.12  lemma suminf_finite:
    1.13    assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    1.14    shows "suminf f = (\<Sum>n\<in>N. f n)"
    1.15 @@ -316,6 +321,12 @@
    1.16  
    1.17  end
    1.18  
    1.19 +lemma summable_minus_iff:
    1.20 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.21 +  shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
    1.22 +  by (auto dest: summable_minus) --{*used two ways, hence must be outside the context above*}
    1.23 +
    1.24 +
    1.25  context
    1.26    fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
    1.27  begin