src/HOL/Analysis/Convex.thy

   then show "f x \<le> b"
     using assms(1)[unfolded convex_on[OF convex_convex_hull], rule_format, of k u v]
     using hull_inc u by fastforce
 qed
 
-lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
-  by (simp add: inner_sum_left sum.If_cases inner_Basis)
-
 lemma convex_set_plus:
   assumes "convex S" and "convex T" shows "convex (S + T)"
 proof -
   have "convex (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
     using assms by (rule convex_sums)