--- a/src/HOL/Analysis/Starlike.thy Wed Dec 04 19:55:30 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Wed Dec 04 23:11:29 2019 +0100
@@ -14,18 +14,6 @@
Line_Segment
begin
-subsection\<open>Starlike sets\<close>
-
-definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
- by (simp add: starlike_def)
-
-lemma convex_imp_starlike:
- "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
- unfolding convex_contains_segment starlike_def by auto
-
-
lemma affine_hull_closed_segment [simp]:
"affine hull (closed_segment a b) = affine hull {a,b}"
by (simp add: segment_convex_hull)
@@ -1003,27 +991,6 @@
lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
-lemma starlike_convex_tweak_boundary_points:
- fixes S :: "'a::euclidean_space set"
- assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
- shows "starlike T"
-proof -
- have "rel_interior S \<noteq> {}"
- by (simp add: assms rel_interior_eq_empty)
- then obtain a where a: "a \<in> rel_interior S" by blast
- with ST have "a \<in> T" by blast
- have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
- apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
- using assms by blast
- show ?thesis
- unfolding starlike_def
- apply (rule bexI [OF _ \<open>a \<in> T\<close>])
- apply (simp add: closed_segment_eq_open)
- apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
- apply (simp add: order_trans [OF * ST])
- done
-qed
-
subsection\<open>The relative frontier of a set\<close>
definition\<^marker>\<open>tag important\<close> "rel_frontier S = closure S - rel_interior S"