changeset 65680 | 378a2f11bec9 |
parent 65583 | 8d53b3bebab4 |
child 66089 | def95e0bc529 |
--- a/src/HOL/Real_Vector_Spaces.thy Tue May 02 10:25:27 2017 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Tue May 02 14:34:06 2017 +0100 @@ -871,7 +871,7 @@ lemma sum_norm_le: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" - assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x" + 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)