549 and starlike_compact_projective2: |
549 and starlike_compact_projective2: |
550 "S homeomorphic cball a 1 \<inter> affine hull S" |
550 "S homeomorphic cball a 1 \<inter> affine hull S" |
551 proof%unimportant - |
551 proof%unimportant - |
552 have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation) |
552 have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation) |
553 have 2: "0 \<in> rel_interior ((+) (-a) ` S)" |
553 have 2: "0 \<in> rel_interior ((+) (-a) ` S)" |
554 by (simp add: a rel_interior_translation) |
554 using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp) |
555 have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x |
555 have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x |
556 proof - |
556 proof - |
557 have "x+a \<in> S" using that by auto |
557 have "x+a \<in> S" using that by auto |
558 then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star) |
558 then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star) |
559 then show ?thesis using open_segment_translation |
559 then show ?thesis using open_segment_translation [of a 0 x] |
560 using rel_interior_translation by fastforce |
560 using rel_interior_translation [of "- a" S] by (fastforce simp add: ac_simps image_iff cong: image_cong_simp) |
561 qed |
561 qed |
562 have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)" |
562 have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)" |
563 by (metis rel_interior_translation translation_diff homeomorphic_translation) |
563 by (metis rel_interior_translation translation_diff homeomorphic_translation) |
564 also have "... homeomorphic sphere 0 1 \<inter> affine hull ((+) (-a) ` S)" |
564 also have "... homeomorphic sphere 0 1 \<inter> affine hull ((+) (-a) ` S)" |
565 by (rule starlike_compact_projective1_0 [OF 1 2 3]) |
565 by (rule starlike_compact_projective1_0 [OF 1 2 3]) |
839 by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl) |
839 by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl) |
840 also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}" |
840 also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}" |
841 using assms by (auto simp: dist_norm norm_minus_commute divide_simps) |
841 using assms by (auto simp: dist_norm norm_minus_commute divide_simps) |
842 also have "... homeomorphic p" |
842 also have "... homeomorphic p" |
843 apply (rule homeomorphic_punctured_affine_sphere_affine_01) |
843 apply (rule homeomorphic_punctured_affine_sphere_affine_01) |
844 using assms |
844 using assms affine_translation [symmetric, of "- a"] aff_dim_translation_eq [of "- a"] |
845 apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj) |
845 apply (auto simp: dist_norm norm_minus_commute affine_scaling inj) |
846 done |
846 done |
847 finally show ?thesis . |
847 finally show ?thesis . |
848 qed |
848 qed |
849 |
849 |
850 corollary%important homeomorphic_punctured_sphere_affine: |
850 corollary%important homeomorphic_punctured_sphere_affine: |
929 have "0 \<in> affine hull ((+) (- a) ` S)" |
929 have "0 \<in> affine hull ((+) (- a) ` S)" |
930 by (simp add: \<open>a \<in> S\<close> hull_inc) |
930 by (simp add: \<open>a \<in> S\<close> hull_inc) |
931 then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)" |
931 then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)" |
932 by (simp add: aff_dim_zero) |
932 by (simp add: aff_dim_zero) |
933 also have "... < DIM('n)" |
933 also have "... < DIM('n)" |
934 by (simp add: aff_dim_translation_eq assms) |
934 by (simp add: aff_dim_translation_eq_subtract assms cong: image_cong_simp) |
935 finally have dd: "dim ((+) (- a) ` S) < DIM('n)" |
935 finally have dd: "dim ((+) (- a) ` S) < DIM('n)" |
936 by linarith |
936 by linarith |
937 obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}" |
937 have span: "span {x. i \<bullet> x = 0} = {x. i \<bullet> x = 0}" |
938 and dimT: "dim T = dim ((+) (- a) ` S)" |
938 using span_eq_iff [symmetric, of "{x. i \<bullet> x = 0}"] subspace_hyperplane [of i] by simp |
939 apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \<bullet> x = 0}"]) |
939 have "dim ((+) (- a) ` S) \<le> dim {x. i \<bullet> x = 0}" |
940 apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>]) |
940 using dd by (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>]) |
941 apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq) |
941 then obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}" |
942 apply (metis span_eq_iff subspace_hyperplane) |
942 and dimT: "dim T = dim ((+) (- a) ` S)" |
943 done |
943 by (rule choose_subspace_of_subspace) (simp add: span) |
944 have "subspace (span ((+) (- a) ` S))" |
944 have "subspace (span ((+) (- a) ` S))" |
945 using subspace_span by blast |
945 using subspace_span by blast |
946 then obtain h k where "linear h" "linear k" |
946 then obtain h k where "linear h" "linear k" |
947 and heq: "h ` span ((+) (- a) ` S) = T" |
947 and heq: "h ` span ((+) (- a) ` S) = T" |
948 and keq:"k ` T = span ((+) (- a) ` S)" |
948 and keq:"k ` T = span ((+) (- a) ` S)" |
972 by (metis image_comp) |
972 by (metis image_comp) |
973 then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1" |
973 then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1" |
974 by (metis Diff_subset order_trans sphere_cball) |
974 by (metis Diff_subset order_trans sphere_cball) |
975 have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1" |
975 have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1" |
976 using gh_sub_sph [THEN subsetD] by (auto simp: o_def) |
976 using gh_sub_sph [THEN subsetD] by (auto simp: o_def) |
977 have ghcont: "continuous_on ((+) (- a) ` S) (\<lambda>x. g (h x))" |
977 have ghcont: "continuous_on ((\<lambda>x. x - a) ` S) (\<lambda>x. g (h x))" |
978 apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force) |
978 apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force) |
979 done |
979 done |
980 have kfcont: "continuous_on ((g \<circ> h \<circ> (+) (- a)) ` S) (\<lambda>x. k (f x))" |
980 have kfcont: "continuous_on ((\<lambda>x. g (h (x - a))) ` S) (\<lambda>x. k (f x))" |
981 apply (rule continuous_on_compose2 [OF kcont]) |
981 apply (rule continuous_on_compose2 [OF kcont]) |
982 using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast) |
982 using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast) |
983 done |
983 done |
984 have "S homeomorphic (+) (- a) ` S" |
984 have "S homeomorphic (+) (- a) ` S" |
985 by (simp add: homeomorphic_translation) |
985 by (fact homeomorphic_translation) |
986 also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S" |
986 also have "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S" |
987 apply (simp add: homeomorphic_def homeomorphism_def) |
987 apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp) |
988 apply (rule_tac x="g \<circ> h" in exI) |
988 apply (rule_tac x="g \<circ> h" in exI) |
989 apply (rule_tac x="k \<circ> f" in exI) |
989 apply (rule_tac x="k \<circ> f" in exI) |
990 apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp) |
990 apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp) |
991 apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base) |
|
992 done |
991 done |
993 finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" . |
992 finally have Shom: "S homeomorphic (\<lambda>x. g (h x)) ` (\<lambda>x. x - a) ` S" |
|
993 by (simp cong: image_cong_simp) |
994 show ?thesis |
994 show ?thesis |
995 apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)" |
995 apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)" |
996 and T = "image (g o h) ((+) (- a) ` S)" |
996 and T = "image (g o h) ((+) (- a) ` S)" |
997 in that) |
997 in that) |
998 apply (rule convex_intermediate_ball [of 0 1], force) |
998 apply (rule convex_intermediate_ball [of 0 1], force) |
999 using gh_sub_cb apply force |
999 using gh_sub_cb apply force |
1000 apply force |
1000 apply force |
1001 apply (simp add: closedin_closed) |
1001 apply (simp add: closedin_closed) |
1002 apply (rule_tac x="sphere 0 1" in exI) |
1002 apply (rule_tac x="sphere 0 1" in exI) |
1003 apply (auto simp: Shom) |
1003 apply (auto simp: Shom cong: image_cong_simp) |
1004 done |
1004 done |
1005 qed |
1005 qed |
1006 |
1006 |
1007 subsection%important\<open>Locally compact sets in an open set\<close> |
1007 subsection%important\<open>Locally compact sets in an open set\<close> |
1008 |
1008 |