--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Sep 13 00:55:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Sep 12 09:03:52 2013 -0700
@@ -322,7 +322,6 @@
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
by (simp add: vec_eq_iff setsum_right_distrib)
-(* TODO: use setsum_norm_allsubsets_bound *)
lemma setsum_norm_allsubsets_bound_cart:
fixes f:: "'a \<Rightarrow> real ^'n"
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"