851 fixes a :: "'a :: euclidean_space" |
851 fixes a :: "'a :: euclidean_space" |
852 assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" |
852 assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" |
853 and "affine T" and affS: "aff_dim S = aff_dim T + 1" |
853 and "affine T" and affS: "aff_dim S = aff_dim T + 1" |
854 shows "rel_frontier S - {a} homeomorphic T" |
854 shows "rel_frontier S - {a} homeomorphic T" |
855 proof - |
855 proof - |
|
856 obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S" |
|
857 using choose_affine_subset [OF affine_UNIV aff_dim_geq] |
|
858 by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex) |
856 have "S \<noteq> {}" using assms by auto |
859 have "S \<noteq> {}" using assms by auto |
857 obtain U :: "'a set" where "affine U" and affdS: "aff_dim U = aff_dim S" |
|
858 using choose_affine_subset [OF affine_UNIV aff_dim_geq] |
|
859 by (meson aff_dim_affine_hull affine_affine_hull) |
|
860 have "convex U" |
|
861 by (simp add: affine_imp_convex \<open>affine U\<close>) |
|
862 have "U \<noteq> {}" |
|
863 by (metis \<open>S \<noteq> {}\<close> \<open>aff_dim U = aff_dim S\<close> aff_dim_empty) |
|
864 then obtain z where "z \<in> U" |
860 then obtain z where "z \<in> U" |
865 by auto |
861 by (metis aff_dim_negative_iff equals0I affdS) |
866 then have bne: "ball z 1 \<inter> U \<noteq> {}" by force |
862 then have bne: "ball z 1 \<inter> U \<noteq> {}" by force |
867 have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U" |
863 then have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U" |
868 using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] bne |
864 using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] |
869 by (fastforce simp add: Int_commute) |
865 by (fastforce simp add: Int_commute) |
870 have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)" |
866 have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)" |
871 apply (rule homeomorphic_rel_frontiers_convex_bounded_sets) |
867 apply (rule homeomorphic_rel_frontiers_convex_bounded_sets) |
872 apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms) |
868 apply (auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms) |
873 done |
869 done |
874 also have "... = sphere z 1 \<inter> U" |
870 also have "... = sphere z 1 \<inter> U" |
875 using convex_affine_rel_frontier_Int [of "ball z 1" U] |
871 using convex_affine_rel_frontier_Int [of "ball z 1" U] |
876 by (simp add: \<open>affine U\<close> bne) |
872 by (simp add: \<open>affine U\<close> bne) |
877 finally obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U" |
873 finally have "rel_frontier S homeomorphic sphere z 1 \<inter> U" . |
|
874 then obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U" |
878 and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S" |
875 and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S" |
879 and hcon: "continuous_on (rel_frontier S) h" |
876 and hcon: "continuous_on (rel_frontier S) h" |
880 and kcon: "continuous_on (sphere z 1 \<inter> U) k" |
877 and kcon: "continuous_on (sphere z 1 \<inter> U) k" |
881 and kh: "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x" |
878 and kh: "\<And>x. x \<in> rel_frontier S \<Longrightarrow> k(h(x)) = x" |
882 and hk: "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y" |
879 and hk: "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y" |
883 unfolding homeomorphic_def homeomorphism_def by auto |
880 unfolding homeomorphic_def homeomorphism_def by auto |
884 have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}" |
881 have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}" |
885 proof (rule homeomorphicI [where f=h and g=k]) |
882 proof (rule homeomorphicI) |
886 show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}" |
883 show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}" |
887 using him a kh by auto metis |
884 using him a kh by auto metis |
888 show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}" |
885 show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}" |
889 by (force simp: h [symmetric] image_comp o_def kh) |
886 by (force simp: h [symmetric] image_comp o_def kh) |
890 qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) |
887 qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) |
891 also have "... homeomorphic T" |
888 also have "... homeomorphic T" |
892 apply (rule homeomorphic_punctured_affine_sphere_affine) |
889 apply (rule homeomorphic_punctured_affine_sphere_affine) |
893 using a him |
890 using a him |
894 by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) |
891 by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) |
895 finally show ?thesis . |
892 finally show ?thesis . |
896 qed |
893 qed |
897 |
894 |
898 |
895 corollary homeomorphic_punctured_sphere_affine: |
899 lemma homeomorphic_punctured_sphere_affine: |
|
900 fixes a :: "'a :: euclidean_space" |
896 fixes a :: "'a :: euclidean_space" |
901 assumes "0 < r" and b: "b \<in> sphere a r" |
897 assumes "0 < r" and b: "b \<in> sphere a r" |
902 and "affine T" and affS: "aff_dim T + 1 = DIM('a)" |
898 and "affine T" and affS: "aff_dim T + 1 = DIM('a)" |
903 shows "(sphere a r - {b}) homeomorphic T" |
899 shows "(sphere a r - {b}) homeomorphic T" |
904 using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T] |
900 using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T] |