825 
825 
826 theorem homeomorphic_punctured_affine_sphere_affine: 
826 theorem homeomorphic_punctured_affine_sphere_affine: 
827 fixes a :: "'a :: euclidean_space" 
827 fixes a :: "'a :: euclidean_space" 
828 assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p" 
828 assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p" 
829 and aff: "aff_dim T = aff_dim p + 1" 
829 and aff: "aff_dim T = aff_dim p + 1" 
830 shows "((sphere a r \<inter> T)  {b}) homeomorphic p" 
830 shows "(sphere a r \<inter> T)  {b} homeomorphic p" 
831 proof  
831 proof  
832 have "a \<noteq> b" using assms by auto 
832 have "a \<noteq> b" using assms by auto 
833 then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a  b))" 
833 then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a  b))" 
834 by (simp add: inj_on_def) 
834 by (simp add: inj_on_def) 
835 have "((sphere a r \<inter> T)  {b}) homeomorphic 
835 have "((sphere a r \<inter> T)  {b}) homeomorphic 
844 using assms 
844 using assms 
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 affine_translation [symmetric] aff_dim_translation_eq inj) 
846 done 
846 done 
847 finally show ?thesis . 
847 finally show ?thesis . 
848 qed 
848 qed 

849 

850 corollary homeomorphic_punctured_sphere_affine: 

851 fixes a :: "'a :: euclidean_space" 

852 assumes "0 < r" and b: "b \<in> sphere a r" 

853 and "affine T" and affS: "aff_dim T + 1 = DIM('a)" 

854 shows "(sphere a r  {b}) homeomorphic T" 

855 using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto 

856 

857 corollary homeomorphic_punctured_sphere_hyperplane: 

858 fixes a :: "'a :: euclidean_space" 

859 assumes "0 < r" and b: "b \<in> sphere a r" 

860 and "c \<noteq> 0" 

861 shows "(sphere a r  {b}) homeomorphic {x::'a. c \<bullet> x = d}" 

862 apply (rule homeomorphic_punctured_sphere_affine) 

863 using assms 

864 apply (auto simp: affine_hyperplane of_nat_diff) 

865 done 
849 
866 
850 proposition homeomorphic_punctured_sphere_affine_gen: 
867 proposition homeomorphic_punctured_sphere_affine_gen: 
851 fixes a :: "'a :: euclidean_space" 
868 fixes a :: "'a :: euclidean_space" 
852 assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" 
869 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" 
870 and "affine T" and affS: "aff_dim S = aff_dim T + 1" 
889 apply (rule homeomorphic_punctured_affine_sphere_affine) 
906 apply (rule homeomorphic_punctured_affine_sphere_affine) 
890 using a him 
907 using a him 
891 by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) 
908 by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>) 
892 finally show ?thesis . 
909 finally show ?thesis . 
893 qed 
910 qed 
894 

895 corollary homeomorphic_punctured_sphere_affine: 

896 fixes a :: "'a :: euclidean_space" 

897 assumes "0 < r" and b: "b \<in> sphere a r" 

898 and "affine T" and affS: "aff_dim T + 1 = DIM('a)" 

899 shows "(sphere a r  {b}) homeomorphic T" 

900 using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T] 

901 assms aff_dim_cball by force 

902 

903 corollary homeomorphic_punctured_sphere_hyperplane: 

904 fixes a :: "'a :: euclidean_space" 

905 assumes "0 < r" and b: "b \<in> sphere a r" 

906 and "c \<noteq> 0" 

907 shows "(sphere a r  {b}) homeomorphic {x::'a. c \<bullet> x = d}" 

908 apply (rule homeomorphic_punctured_sphere_affine) 

909 using assms 

910 apply (auto simp: affine_hyperplane of_nat_diff) 

911 done 

912 
911 
913 
912 
914 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set 
913 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set 
915 is homeomorphic to a closed subset of a convex set, and 
914 is homeomorphic to a closed subset of a convex set, and 
916 if the set is locally compact we can take the convex set to be the universe.\<close> 
915 if the set is locally compact we can take the convex set to be the universe.\<close> 