--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Apr 30 13:51:17 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat May 01 07:35:22 2010 -0700
@@ -2205,14 +2205,6 @@
subsection {* Use this to derive general bound property of convex function. *}
-(* TODO: move *)
-lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
-(* TODO: move *)
-lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
-
lemma convex_on:
assumes "convex s"
shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>