src/HOL/Analysis/Linear_Algebra.thy
changeset 65680 378a2f11bec9
parent 64773 223b2ebdda79
child 66287 005a30862ed0
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 10:25:27 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 14:34:06 2017 +0100
     1.3 @@ -1480,12 +1480,6 @@
     1.4      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
     1.5    by (auto simp add: insert_absorb)
     1.6  
     1.7 -lemma sum_norm_le:
     1.8 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.9 -  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
    1.10 -  shows "norm (sum f S) \<le> sum g S"
    1.11 -  by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
    1.12 -
    1.13  lemma sum_norm_bound:
    1.14    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.15    assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"