moved starlike where it belongs
authornipkow
Wed Dec 04 23:11:29 2019 +0100 (44 hours ago ago)
changeset 71436da28fd2852ed
parent 71435 7b9ff966974f
child 71437 f1838cf9f139
moved starlike where it belongs
src/HOL/Analysis/Homotopy.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Wed Dec 04 19:55:30 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Wed Dec 04 23:11:29 2019 +0100
     1.3 @@ -1478,6 +1478,38 @@
     1.4  using homotopic_through_contractible [of S id S f T id g]
     1.5  by (simp add: assms contractible_imp_path_connected)
     1.6  
     1.7 +subsection\<open>Starlike sets\<close>
     1.8 +
     1.9 +definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
    1.10 +
    1.11 +lemma starlike_UNIV [simp]: "starlike UNIV"
    1.12 +  by (simp add: starlike_def)
    1.13 +
    1.14 +lemma convex_imp_starlike:
    1.15 +  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
    1.16 +  unfolding convex_contains_segment starlike_def by auto
    1.17 +
    1.18 +lemma starlike_convex_tweak_boundary_points:
    1.19 +  fixes S :: "'a::euclidean_space set"
    1.20 +  assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
    1.21 +  shows "starlike T"
    1.22 +proof -
    1.23 +  have "rel_interior S \<noteq> {}"
    1.24 +    by (simp add: assms rel_interior_eq_empty)
    1.25 +  then obtain a where a: "a \<in> rel_interior S"  by blast
    1.26 +  with ST have "a \<in> T"  by blast
    1.27 +  have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
    1.28 +    apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    1.29 +    using assms by blast
    1.30 +  show ?thesis
    1.31 +    unfolding starlike_def
    1.32 +    apply (rule bexI [OF _ \<open>a \<in> T\<close>])
    1.33 +    apply (simp add: closed_segment_eq_open)
    1.34 +    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    1.35 +    apply (simp add: order_trans [OF * ST])
    1.36 +    done
    1.37 +qed
    1.38 +
    1.39  lemma starlike_imp_contractible_gen:
    1.40    fixes S :: "'a::real_normed_vector set"
    1.41    assumes S: "starlike S"
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 19:55:30 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 23:11:29 2019 +0100
     2.3 @@ -14,18 +14,6 @@
     2.4      Line_Segment
     2.5  begin
     2.6  
     2.7 -subsection\<open>Starlike sets\<close>
     2.8 -
     2.9 -definition\<^marker>\<open>tag important\<close> "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
    2.10 -
    2.11 -lemma starlike_UNIV [simp]: "starlike UNIV"
    2.12 -  by (simp add: starlike_def)
    2.13 -
    2.14 -lemma convex_imp_starlike:
    2.15 -  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
    2.16 -  unfolding convex_contains_segment starlike_def by auto
    2.17 -
    2.18 -
    2.19  lemma affine_hull_closed_segment [simp]:
    2.20       "affine hull (closed_segment a b) = affine hull {a,b}"
    2.21    by (simp add: segment_convex_hull)
    2.22 @@ -1003,27 +991,6 @@
    2.23  
    2.24  lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
    2.25  
    2.26 -lemma starlike_convex_tweak_boundary_points:
    2.27 -  fixes S :: "'a::euclidean_space set"
    2.28 -  assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
    2.29 -  shows "starlike T"
    2.30 -proof -
    2.31 -  have "rel_interior S \<noteq> {}"
    2.32 -    by (simp add: assms rel_interior_eq_empty)
    2.33 -  then obtain a where a: "a \<in> rel_interior S"  by blast
    2.34 -  with ST have "a \<in> T"  by blast
    2.35 -  have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
    2.36 -    apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    2.37 -    using assms by blast
    2.38 -  show ?thesis
    2.39 -    unfolding starlike_def
    2.40 -    apply (rule bexI [OF _ \<open>a \<in> T\<close>])
    2.41 -    apply (simp add: closed_segment_eq_open)
    2.42 -    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    2.43 -    apply (simp add: order_trans [OF * ST])
    2.44 -    done
    2.45 -qed
    2.46 -
    2.47  subsection\<open>The relative frontier of a set\<close>
    2.48  
    2.49  definition\<^marker>\<open>tag important\<close> "rel_frontier S = closure S - rel_interior S"