--- a/src/HOL/Analysis/Line_Segment.thy Wed Dec 04 15:36:58 2019 +0100
+++ b/src/HOL/Analysis/Line_Segment.thy Wed Dec 04 18:28:24 2019 +0100
@@ -789,6 +789,57 @@
lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
+lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
+ by auto
+
+lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
+proof -
+ { assume a1: "open_segment a b = {}"
+ have "{} \<noteq> {0::real<..<1}"
+ by simp
+ then have "a = b"
+ using a1 open_segment_image_interval by fastforce
+ } then show ?thesis by auto
+qed
+
+lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
+ using open_segment_eq_empty by blast
+
+lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
+
+lemma inj_segment:
+ fixes a :: "'a :: real_vector"
+ assumes "a \<noteq> b"
+ shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
+proof
+ fix x y
+ assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
+ then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
+ by (simp add: algebra_simps)
+ with assms show "x = y"
+ by (simp add: real_vector.scale_right_imp_eq)
+qed
+
+lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
+ apply auto
+ apply (rule ccontr)
+ apply (simp add: segment_image_interval)
+ using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
+ done
+
+lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
+ by (auto simp: open_segment_def)
+
+lemmas finite_segment = finite_closed_segment finite_open_segment
+
+lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
+ by auto
+
+lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
+ by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
+
+lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
+
lemma open_segment_bound1:
assumes "x \<in> open_segment a b"
shows "norm (x - a) < norm (b - a)"
@@ -868,6 +919,172 @@
lemmas convex_segment = convex_closed_segment convex_open_segment
+lemma subset_closed_segment:
+ "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+ a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+ by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
+
+lemma subset_co_segment:
+ "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+ a \<in> open_segment c d \<and> b \<in> open_segment c d"
+using closed_segment_subset by blast
+
+lemma subset_open_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+ a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+ (is "?lhs = ?rhs")
+proof (cases "a = b")
+ case True then show ?thesis by simp
+next
+ case False show ?thesis
+ proof
+ assume rhs: ?rhs
+ with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+ using closed_segment_idem singleton_iff by auto
+ have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
+ (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
+ if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
+ and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
+ and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
+ for u ua ub
+ proof -
+ have "ua \<noteq> ub"
+ using neq by auto
+ moreover have "(u - 1) * ua \<le> 0" using u uab
+ by (simp add: mult_nonpos_nonneg)
+ ultimately have lt: "(u - 1) * ua < u * ub" using u uab
+ by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
+ have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q
+ proof -
+ have "\<not> p \<le> 0" "\<not> q \<le> 0"
+ using p q not_less by blast+
+ then show ?thesis
+ by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
+ less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
+ qed
+ then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
+ by (metis diff_add_cancel diff_gt_0_iff_gt)
+ with lt show ?thesis
+ by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
+ qed
+ with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
+ unfolding open_segment_image_interval closed_segment_def
+ by (fastforce simp add:)
+ next
+ assume lhs: ?lhs
+ with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+ by (meson finite_open_segment rev_finite_subset)
+ have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
+ using lhs closure_mono by blast
+ then have "closed_segment a b \<subseteq> closed_segment c d"
+ by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
+ then show ?rhs
+ by (force simp: \<open>a \<noteq> b\<close>)
+ qed
+qed
+
+lemma subset_oc_segment:
+ fixes a :: "'a::euclidean_space"
+ shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+ a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+apply (simp add: subset_open_segment [symmetric])
+apply (rule iffI)
+ apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
+apply (meson dual_order.trans segment_open_subset_closed)
+done
+
+lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
+
+lemma dist_half_times2:
+ fixes a :: "'a :: real_normed_vector"
+ shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
+proof -
+ have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
+ by simp
+ also have "... = norm ((a + b) - 2 *\<^sub>R x)"
+ by (simp add: real_vector.scale_right_diff_distrib)
+ finally show ?thesis
+ by (simp only: dist_norm)
+qed
+
+lemma closed_segment_as_ball:
+ "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+ case True then show ?thesis by (auto simp: hull_inc)
+next
+ case False
+ then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+ (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
+ proof -
+ have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+ ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
+ unfolding eq_diff_eq [symmetric] by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
+ by (simp add: dist_half_times2) (simp add: dist_norm)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
+ by auto
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
+ by (simp add: algebra_simps scaleR_2)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
+ by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
+ by (simp add: mult_le_cancel_right2 False)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
+ by auto
+ finally show ?thesis .
+ qed
+ show ?thesis
+ by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
+qed
+
+lemma open_segment_as_ball:
+ "open_segment a b =
+ affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+ case True then show ?thesis by (auto simp: hull_inc)
+next
+ case False
+ then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+ (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
+ proof -
+ have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+ ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+ dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
+ unfolding eq_diff_eq [symmetric] by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
+ by (simp add: dist_half_times2) (simp add: dist_norm)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
+ by auto
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
+ by (simp add: algebra_simps scaleR_2)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+ \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
+ by simp
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
+ by (simp add: mult_le_cancel_right2 False)
+ also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
+ by auto
+ finally show ?thesis .
+ qed
+ show ?thesis
+ using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
+qed
+
+lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
+
lemma connected_segment [iff]:
fixes x :: "'a :: real_normed_vector"
shows "connected (closed_segment x y)"
--- a/src/HOL/Analysis/Starlike.thy Wed Dec 04 15:36:58 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Wed Dec 04 18:28:24 2019 +0100
@@ -79,226 +79,6 @@
by (meson hull_mono inf_mono subset_insertI subset_refl)
qed
-subsection\<^marker>\<open>tag unimportant\<close>\<open>More results about segments\<close>
-
-lemma dist_half_times2:
- fixes a :: "'a :: real_normed_vector"
- shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
-proof -
- have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
- by simp
- also have "... = norm ((a + b) - 2 *\<^sub>R x)"
- by (simp add: real_vector.scale_right_diff_distrib)
- finally show ?thesis
- by (simp only: dist_norm)
-qed
-
-lemma closed_segment_as_ball:
- "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
-proof (cases "b = a")
- case True then show ?thesis by (auto simp: hull_inc)
-next
- case False
- then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
- (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
- proof -
- have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
- ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
- unfolding eq_diff_eq [symmetric] by simp
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
- by (simp add: dist_half_times2) (simp add: dist_norm)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
- by auto
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
- by (simp add: algebra_simps scaleR_2)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
- by simp
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
- by (simp add: mult_le_cancel_right2 False)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
- by auto
- finally show ?thesis .
- qed
- show ?thesis
- by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
-qed
-
-lemma open_segment_as_ball:
- "open_segment a b =
- affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
-proof (cases "b = a")
- case True then show ?thesis by (auto simp: hull_inc)
-next
- case False
- then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
- (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
- proof -
- have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
- ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
- dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
- unfolding eq_diff_eq [symmetric] by simp
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
- by (simp add: dist_half_times2) (simp add: dist_norm)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
- by auto
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
- by (simp add: algebra_simps scaleR_2)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
- \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
- by simp
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
- by (simp add: mult_le_cancel_right2 False)
- also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
- by auto
- finally show ?thesis .
- qed
- show ?thesis
- using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
-qed
-
-lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
-
-lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
- by auto
-
-lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
-proof -
- { assume a1: "open_segment a b = {}"
- have "{} \<noteq> {0::real<..<1}"
- by simp
- then have "a = b"
- using a1 open_segment_image_interval by fastforce
- } then show ?thesis by auto
-qed
-
-lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
- using open_segment_eq_empty by blast
-
-lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
-
-lemma inj_segment:
- fixes a :: "'a :: real_vector"
- assumes "a \<noteq> b"
- shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
-proof
- fix x y
- assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
- then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
- by (simp add: algebra_simps)
- with assms show "x = y"
- by (simp add: real_vector.scale_right_imp_eq)
-qed
-
-lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
- apply auto
- apply (rule ccontr)
- apply (simp add: segment_image_interval)
- using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
- done
-
-lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
- by (auto simp: open_segment_def)
-
-lemmas finite_segment = finite_closed_segment finite_open_segment
-
-lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
- by auto
-
-lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
- by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
-
-lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
-
-lemma subset_closed_segment:
- "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
- a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
- by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
-
-lemma subset_co_segment:
- "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
- a \<in> open_segment c d \<and> b \<in> open_segment c d"
-using closed_segment_subset by blast
-
-lemma subset_open_segment:
- fixes a :: "'a::euclidean_space"
- shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
- a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
- (is "?lhs = ?rhs")
-proof (cases "a = b")
- case True then show ?thesis by simp
-next
- case False show ?thesis
- proof
- assume rhs: ?rhs
- with \<open>a \<noteq> b\<close> have "c \<noteq> d"
- using closed_segment_idem singleton_iff by auto
- have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
- (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
- if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
- and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
- and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
- for u ua ub
- proof -
- have "ua \<noteq> ub"
- using neq by auto
- moreover have "(u - 1) * ua \<le> 0" using u uab
- by (simp add: mult_nonpos_nonneg)
- ultimately have lt: "(u - 1) * ua < u * ub" using u uab
- by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
- have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q
- proof -
- have "\<not> p \<le> 0" "\<not> q \<le> 0"
- using p q not_less by blast+
- then show ?thesis
- by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
- less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
- qed
- then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
- by (metis diff_add_cancel diff_gt_0_iff_gt)
- with lt show ?thesis
- by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
- qed
- with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
- unfolding open_segment_image_interval closed_segment_def
- by (fastforce simp add:)
- next
- assume lhs: ?lhs
- with \<open>a \<noteq> b\<close> have "c \<noteq> d"
- by (meson finite_open_segment rev_finite_subset)
- have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
- using lhs closure_mono by blast
- then have "closed_segment a b \<subseteq> closed_segment c d"
- by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
- then show ?rhs
- by (force simp: \<open>a \<noteq> b\<close>)
- qed
-qed
-
-lemma subset_oc_segment:
- fixes a :: "'a::euclidean_space"
- shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
- a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-apply (simp add: subset_open_segment [symmetric])
-apply (rule iffI)
- apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
-apply (meson dual_order.trans segment_open_subset_closed)
-done
-
-lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
-
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
lemma mem_interior_convex_shrink: