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
```