src/HOL/Analysis/Homeomorphism.thy
 changeset 66710 676258a1cf01 parent 66690 6953b1a29e19 child 66827 c94531b5007d
equal inserted replaced
66709:b034d2ae541c 66710:676258a1cf01
`   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`
`   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>`