# HG changeset patch # User huffman # Date 1315264060 25200 # Node ID 8478eab380e9af177cb4ccaf2a60d27bc5c2b49e # Parent d3bf0e33c98a60f79d20654d8b1d355c9a7c240c generalize some lemmas diff -r d3bf0e33c98a -r 8478eab380e9 src/HOL/Series.thy --- a/src/HOL/Series.thy Mon Sep 05 12:19:04 2011 -0700 +++ b/src/HOL/Series.thy Mon Sep 05 16:07:40 2011 -0700 @@ -435,7 +435,7 @@ by (simp add: summable_def sums_def convergent_def) lemma summable_LIMSEQ_zero: - fixes f :: "nat \ 'a::real_normed_field" + fixes f :: "nat \ 'a::real_normed_vector" shows "summable f \ f ----> 0" apply (drule summable_convergent_sumr_iff [THEN iffD1]) apply (drule convergent_Cauchy) diff -r d3bf0e33c98a -r 8478eab380e9 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Sep 05 12:19:04 2011 -0700 +++ b/src/HOL/Transcendental.thy Mon Sep 05 16:07:40 2011 -0700 @@ -54,7 +54,7 @@ x}, then it sums absolutely for @{term z} with @{term "\z\ < \x\"}.*} lemma powser_insidea: - fixes x z :: "'a::{real_normed_field,banach}" + fixes x z :: "'a::real_normed_field" assumes 1: "summable (\n. f n * x ^ n)" assumes 2: "norm z < norm x" shows "summable (\n. norm (f n * z ^ n))" @@ -65,7 +65,7 @@ hence "convergent (\n. f n * x ^ n)" by (rule convergentI) hence "Cauchy (\n. f n * x ^ n)" - by (simp add: Cauchy_convergent_iff) + by (rule convergent_Cauchy) hence "Bseq (\n. f n * x ^ n)" by (rule Cauchy_Bseq) then obtain K where 3: "0 < K" and 4: "\n. norm (f n * x ^ n) \ K"