153 using a by simp |
153 using a by simp |
154 then show ?thesis |
154 then show ?thesis |
155 apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>]) |
155 apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> _ _ \<open>l \<noteq> 0\<close>]) |
156 using a affine_hull_nonempty_interior apply blast |
156 using a affine_hull_nonempty_interior apply blast |
157 by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that) |
157 by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that) |
|
158 qed |
|
159 |
|
160 |
|
161 lemma segment_to_rel_frontier_aux: |
|
162 fixes x :: "'a::euclidean_space" |
|
163 assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y" |
|
164 obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z" |
|
165 "open_segment x z \<subseteq> rel_interior S" |
|
166 proof - |
|
167 have "x + (y - x) \<in> affine hull S" |
|
168 using hull_inc [OF y] by auto |
|
169 then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S" |
|
170 and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S" |
|
171 by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto) |
|
172 show ?thesis |
|
173 proof |
|
174 show "x + d *\<^sub>R (y - x) \<in> rel_frontier S" |
|
175 by (simp add: df) |
|
176 next |
|
177 have "open_segment x y \<subseteq> rel_interior S" |
|
178 using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast |
|
179 moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1" |
|
180 using xy |
|
181 apply (auto simp: in_segment) |
|
182 apply (rule_tac x="d" in exI) |
|
183 using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps) |
|
184 done |
|
185 ultimately have "1 \<le> d" |
|
186 using df rel_frontier_def by fastforce |
|
187 moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x" |
|
188 by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one) |
|
189 ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))" |
|
190 apply (auto simp: in_segment) |
|
191 apply (rule_tac x="1/d" in exI) |
|
192 apply (auto simp: divide_simps algebra_simps) |
|
193 done |
|
194 next |
|
195 show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S" |
|
196 apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x]) |
|
197 using df rel_frontier_def by auto |
|
198 qed |
|
199 qed |
|
200 |
|
201 lemma segment_to_rel_frontier: |
|
202 fixes x :: "'a::euclidean_space" |
|
203 assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S" |
|
204 and y: "y \<in> S" and xy: "~(x = y \<and> S = {x})" |
|
205 obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z" |
|
206 "open_segment x z \<subseteq> rel_interior S" |
|
207 proof (cases "x=y") |
|
208 case True |
|
209 with xy have "S \<noteq> {x}" |
|
210 by blast |
|
211 with True show ?thesis |
|
212 by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y) |
|
213 next |
|
214 case False |
|
215 then show ?thesis |
|
216 using segment_to_rel_frontier_aux [OF S x y] that by blast |
158 qed |
217 qed |
159 |
218 |
160 proposition rel_frontier_not_sing: |
219 proposition rel_frontier_not_sing: |
161 fixes a :: "'a::euclidean_space" |
220 fixes a :: "'a::euclidean_space" |
162 assumes "bounded S" |
221 assumes "bounded S" |