changeset 77490 | 2c86ea8961b5 |
parent 74729 | 64b3d8d9bd10 |
child 78475 | a5f6d2fc1b1f |
--- a/src/HOL/Analysis/Convex.thy Thu Mar 02 11:34:54 2023 +0000 +++ b/src/HOL/Analysis/Convex.thy Thu Mar 02 17:17:18 2023 +0000 @@ -2369,9 +2369,6 @@ 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 -