author nipkow Tue, 05 Nov 2019 19:13:47 +0100 changeset 71040 9d2753406c60 parent 71033 c1b63124245c child 71041 fdb6c5034c24
removed redundant lemma
 src/HOL/Analysis/Convex.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Convex.thy	Tue Nov 05 14:57:41 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Tue Nov 05 19:13:47 2019 +0100
@@ -2696,8 +2696,7 @@
proof -
obtain s u where s_u: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
using assms affine_hull_explicit[of S] by auto
-  then have "\<exists>v\<in>s. u v \<noteq> 0"
-    using sum_not_0[of "u" "s"] by auto
+  then have "\<exists>v\<in>s. u v \<noteq> 0" by auto
then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)"
using s_u by auto
then show ?thesis
@@ -3483,7 +3482,7 @@
have "sum c s = 0"
moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
-      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum_not_0 zero_neq_one)
+      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
by (simp add: c_def if_smult sum_negf
```--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 14:57:41 2019 +0100