src/HOL/Real_Vector_Spaces.thy
changeset 56194 9ffbb4004c81
parent 55719 cdddd073bff8
child 56369 2704ca85be98
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 18 15:53:48 2014 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 18 16:29:32 2014 +0100
     1.3 @@ -747,6 +747,11 @@
     1.4    shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
     1.5  by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
     1.6  
     1.7 +lemma norm_setsum:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.9 +  shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
    1.10 +  by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
    1.11 +
    1.12  lemma abs_norm_cancel [simp]:
    1.13    fixes a :: "'a::real_normed_vector"
    1.14    shows "\<bar>norm a\<bar> = norm a"