# HG changeset patch
# User nipkow
# Date 1575497489 -3600
# Node ID da28fd2852ed21fe6c3ce2dea199c8c21c92e2dd
# Parent  7b9ff966974f9657a39a682cd7eb0f39c159d2b5
moved starlike where it belongs

diff -r 7b9ff966974f -r da28fd2852ed src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Wed Dec 04 19:55:30 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Wed Dec 04 23:11:29 2019 +0100
@@ -1478,6 +1478,38 @@
 using homotopic_through_contractible [of S id S f T id g]
 by (simp add: assms contractible_imp_path_connected)
 
+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 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
+
 lemma starlike_imp_contractible_gen:
   fixes S :: "'a::real_normed_vector set"
   assumes S: "starlike S"
diff -r 7b9ff966974f -r da28fd2852ed src/HOL/Analysis/Starlike.thy
--- 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"