src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
 changeset 44170 510ac30f44c0 parent 44142 8e27e0177518 child 44282 f0de18b62d63
```     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
1.3 @@ -101,9 +101,9 @@
1.4
1.5  lemma span_eq[simp]: "(span s = s) <-> subspace s"
1.6  proof-
1.7 -  { fix f assume "f <= subspace"
1.8 -    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto  }
1.9 -  thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
1.10 +  { fix f assume "Ball f subspace"
1.11 +    hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto  }
1.12 +  thus ?thesis using hull_eq[of subspace s] span_def by auto
1.13  qed
1.14
1.15  lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
1.16 @@ -391,11 +391,11 @@
1.17    unfolding affine_def by auto
1.18
1.19  lemma affine_affine_hull: "affine(affine hull s)"
1.20 -  unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
1.21 -  unfolding mem_def by auto
1.22 +  unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"]
1.23 +  by auto
1.24
1.25  lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
1.26 -by (metis affine_affine_hull hull_same mem_def)
1.27 +by (metis affine_affine_hull hull_same)
1.28
1.29  subsection {* Some explicit formulations (from Lars Schewe). *}
1.30
1.31 @@ -459,7 +459,7 @@
1.32
1.33  lemma affine_hull_explicit:
1.34    "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"
1.35 -  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
1.36 +  apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq
1.37    apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
1.38    fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
1.39      apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
1.40 @@ -500,7 +500,7 @@
1.41  subsection {* Stepping theorems and hence small special cases. *}
1.42
1.43  lemma affine_hull_empty[simp]: "affine hull {} = {}"
1.44 -  apply(rule hull_unique) unfolding mem_def by auto
1.45 +  apply(rule hull_unique) by auto
1.46
1.47  lemma affine_hull_finite_step:
1.48    fixes y :: "'a::real_vector"
1.49 @@ -812,12 +812,11 @@
1.50  subsection {* Conic hull. *}
1.51
1.52  lemma cone_cone_hull: "cone (cone hull s)"
1.53 -  unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"]
1.54 -  by (auto simp add: mem_def)
1.55 +  unfolding hull_def by auto
1.56
1.57  lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
1.58 -  apply(rule hull_eq[unfolded mem_def])
1.59 -  using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
1.60 +  apply(rule hull_eq)
1.61 +  using cone_Inter unfolding subset_eq by auto
1.62
1.63  lemma mem_cone:
1.64    assumes "cone S" "x : S" "c>=0"
1.65 @@ -888,7 +887,7 @@
1.66  lemma mem_cone_hull:
1.67    assumes "x : S" "c>=0"
1.68    shows "c *\<^sub>R x : cone hull S"
1.69 -by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
1.70 +by (metis assms cone_cone_hull hull_inc mem_cone)
1.71
1.72  lemma cone_hull_expl:
1.73  fixes S :: "('m::euclidean_space) set"
1.74 @@ -901,11 +900,11 @@
1.75    moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
1.76    ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
1.77  } hence "cone ?rhs" unfolding cone_def by auto
1.78 -  hence "?rhs : cone" unfolding mem_def by auto
1.79 +  hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto
1.80  { fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
1.81    hence "x : ?rhs" by auto
1.82  } hence "S <= ?rhs" by auto
1.83 -hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
1.84 +hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
1.85  moreover
1.86  { fix x assume "x : ?rhs"
1.87    from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
1.88 @@ -1081,18 +1080,18 @@
1.89  subsection {* Convex hull. *}
1.90
1.91  lemma convex_convex_hull: "convex(convex hull s)"
1.92 -  unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
1.93 -  unfolding mem_def by auto
1.94 +  unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
1.95 +  by auto
1.96
1.97  lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
1.98 -by (metis convex_convex_hull hull_same mem_def)
1.99 +by (metis convex_convex_hull hull_same)
1.100
1.101  lemma bounded_convex_hull:
1.102    fixes s :: "'a::real_normed_vector set"
1.103    assumes "bounded s" shows "bounded(convex hull s)"
1.104  proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
1.105    show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
1.106 -    unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
1.107 +    unfolding subset_hull[of convex, OF convex_cball]
1.108      unfolding subset_eq mem_cball dist_norm using B by auto qed
1.109
1.110  lemma finite_imp_bounded_convex_hull:
1.111 @@ -1125,17 +1124,17 @@
1.112  subsection {* Stepping theorems for convex hulls of finite sets. *}
1.113
1.114  lemma convex_hull_empty[simp]: "convex hull {} = {}"
1.115 -  apply(rule hull_unique) unfolding mem_def by auto
1.116 +  apply(rule hull_unique) by auto
1.117
1.118  lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
1.119 -  apply(rule hull_unique) unfolding mem_def by auto
1.120 +  apply(rule hull_unique) by auto
1.121
1.122  lemma convex_hull_insert:
1.123    fixes s :: "'a::real_vector set"
1.124    assumes "s \<noteq> {}"
1.125    shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
1.126                                      b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
1.127 - apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
1.128 + apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
1.129   fix x assume x:"x = a \<or> x \<in> s"
1.130   thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
1.131     apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
1.132 @@ -1192,7 +1191,7 @@
1.133    shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
1.134                              (setsum u {1..k} = 1) \<and>
1.135                              (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
1.136 -  apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
1.137 +  apply(rule hull_unique) apply(rule) defer
1.138    apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
1.139  proof-
1.140    fix x assume "x\<in>s"
1.141 @@ -1232,7 +1231,7 @@
1.142    assumes "finite s"
1.143    shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
1.144           setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
1.145 -proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
1.146 +proof(rule hull_unique, auto simp add: convex_def[of ?set])
1.147    fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
1.148      apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
1.149      unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
1.150 @@ -1356,8 +1355,8 @@
1.151    apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
1.152
1.153  lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u.  0 \<le> u \<and> u \<le> 1}"
1.154 -  unfolding convex_hull_2 unfolding Collect_def
1.155 -proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
1.156 +  unfolding convex_hull_2
1.157 +proof(rule Collect_cong) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
1.158    fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"
1.159      unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
1.160
1.161 @@ -1367,8 +1366,8 @@
1.162    have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
1.163    have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
1.164           "\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
1.165 -  show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
1.166 -    unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
1.167 +  show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
1.168 +    unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto
1.169      apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
1.170      apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed
1.171
1.172 @@ -1392,14 +1391,14 @@
1.173
1.174  lemma affine_hull_subset_span:
1.175    fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
1.176 -by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)
1.177 +by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
1.178
1.179  lemma convex_hull_subset_span:
1.180    fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
1.181 -by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)
1.182 +by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
1.183
1.184  lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
1.185 -by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)
1.186 +by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
1.187
1.188
1.189  lemma affine_dependent_imp_dependent:
1.190 @@ -1572,11 +1571,11 @@
1.191  proof-
1.192  have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
1.193  moreover have "(%x. a + x) `  S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
1.194 -ultimately have h1: "affine hull ((%x. a + x) `  S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
1.195 +ultimately have h1: "affine hull ((%x. a + x) `  S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal)
1.196  have "affine((%x. -a + x) ` (affine hull ((%x. a + x) `  S)))"  using affine_translation affine_affine_hull by auto
1.197  moreover have "(%x. -a + x) ` (%x. a + x) `  S <= (%x. -a + x) ` (affine hull ((%x. a + x) `  S))" using hull_subset[of "(%x. a + x) `  S"] by auto
1.198  moreover have "S=(%x. -a + x) ` (%x. a + x) `  S" using  translation_assoc[of "-a" a] by auto
1.199 -ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) `  S)) >= (affine hull S)" by (metis hull_minimal mem_def)
1.200 +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) `  S)) >= (affine hull S)" by (metis hull_minimal)
1.201  hence "affine hull ((%x. a + x) `  S) >= (%x. a + x) ` (affine hull S)" by auto
1.202  from this show ?thesis using h1 by auto
1.203  qed
1.204 @@ -3016,7 +3015,7 @@
1.205      then obtain a b where ab:"a \<noteq> 0" "0 < b"  "\<forall>x\<in>convex hull c. b < inner a x"
1.206        using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
1.207        using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
1.208 -      using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto
1.209 +      using subset_hull[of convex, OF assms(1), THEN sym, of c] by auto
1.210      hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
1.211         using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
1.212         apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
1.213 @@ -3077,7 +3076,7 @@
1.214
1.215  lemma convex_hull_translation_lemma:
1.216    "convex hull ((\<lambda>x. a + x) ` s) \<subseteq> (\<lambda>x. a + x) ` (convex hull s)"
1.217 -by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def)
1.218 +by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono)
1.219
1.220  lemma convex_hull_bilemma: fixes neg
1.221    assumes "(\<forall>s a. (convex hull (up a s)) \<subseteq> up a (convex hull s))"
1.222 @@ -3091,7 +3090,7 @@
1.223
1.224  lemma convex_hull_scaling_lemma:
1.225   "(convex hull ((\<lambda>x. c *\<^sub>R x) ` s)) \<subseteq> (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
1.226 -by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff)
1.227 +by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff)
1.228
1.229  lemma convex_hull_scaling:
1.230    "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
1.231 @@ -3269,7 +3268,7 @@
1.232        unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
1.233      have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
1.234      have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
1.235 -      apply(rule_tac [!] hull_minimal) using Suc gh(3-4)  unfolding mem_def unfolding subset_eq
1.236 +      apply(rule_tac [!] hull_minimal) using Suc gh(3-4)  unfolding subset_eq
1.237        apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof-
1.238        fix x assume "x\<in>X ` g" then guess y unfolding image_iff ..
1.239        thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
1.240 @@ -3710,7 +3709,7 @@
1.241      apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
1.242      apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
1.243      unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
1.244 -    by(auto simp add: mem_def[of _ convex]) qed
1.245 +    by auto qed
1.246
1.247  subsection {* And this is a finite set of vertices. *}
1.248
1.249 @@ -3883,7 +3882,7 @@
1.250    closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
1.251    "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
1.252
1.253 -definition "between = (\<lambda> (a,b). closed_segment a b)"
1.254 +definition "between = (\<lambda> (a,b) x. x \<in> closed_segment a b)"
1.255
1.256  lemmas segment = open_segment_def closed_segment_def
1.257
1.258 @@ -3968,15 +3967,15 @@
1.259  lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
1.260
1.261  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
1.262 -  unfolding between_def mem_def by auto
1.263 +  unfolding between_def by auto
1.264
1.265  lemma between:"between (a,b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
1.266  proof(cases "a = b")
1.267 -  case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
1.268 +  case True thus ?thesis unfolding between_def split_conv
1.269      by(auto simp add:segment_refl dist_commute) next
1.270    case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto
1.271    have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)
1.272 -  show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq
1.273 +  show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq
1.274      apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof-
1.275        fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
1.276        hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
1.277 @@ -4743,8 +4742,8 @@
1.278    { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
1.279    hence "y : Inter {closure S |S. S : I}" by auto
1.280  } hence "Inter I <= Inter {closure S |S. S : I}" by auto
1.281 -moreover have "Inter {closure S |S. S : I} : closed"
1.282 -  unfolding mem_def closed_Inter closed_closure by auto
1.283 +moreover have "closed (Inter {closure S |S. S : I})"
1.284 +  unfolding closed_Inter closed_closure by auto
1.285  ultimately show ?thesis using closure_hull[of "Inter I"]
1.286    hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
1.287  qed
1.288 @@ -5074,8 +5073,8 @@
1.289       using I_def u_def by auto
1.290  }
1.291  hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
1.292 -moreover have "(convex hull S) <*> (convex hull T) : convex"
1.293 -   unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull)
1.294 +moreover have "convex ((convex hull S) <*> (convex hull T))"
1.295 +   by (simp add: convex_direct_sum convex_convex_hull)
1.296  ultimately show ?thesis
1.297     using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"]
1.298           hull_subset[of S convex] hull_subset[of T convex] by auto
1.299 @@ -5384,7 +5383,6 @@
1.300    finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
1.301    hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
1.302  } hence "convex ?rhs" unfolding convex_def by auto
1.303 -hence "?rhs : convex" unfolding mem_def by auto
1.304  from this show ?thesis using `?lhs >= ?rhs` *
1.305     hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
1.306  qed
1.307 @@ -5578,7 +5576,7 @@
1.308      hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
1.309    }
1.310    hence "K0 >= Union (K ` I)" by auto
1.311 -  moreover have "K0 : convex" unfolding mem_def K0_def
1.312 +  moreover have "convex K0" unfolding K0_def
1.313       apply (subst convex_cone_hull) apply (subst convex_direct_sum)
1.314       unfolding C0_def using convex_convex_hull by auto
1.315    ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
1.316 @@ -5587,7 +5585,7 @@
1.317    hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
1.318    hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
1.319       using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
1.320 -  moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull)
1.321 +  moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
1.322       using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
1.323    ultimately have "convex hull (Union (K ` I)) >= K0"
1.324       unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
```