--- a/src/HOL/Analysis/Linear_Algebra.thy Tue May 02 10:25:27 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue May 02 14:34:06 2017 +0100
@@ -1480,12 +1480,6 @@
and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
by (auto simp add: insert_absorb)
-lemma sum_norm_le:
- fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
- shows "norm (sum f S) \<le> sum g S"
- by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
-
lemma sum_norm_bound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"