summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Analysis/Homeomorphism.thy

changeset 66710 | 676258a1cf01 |

parent 66690 | 6953b1a29e19 |

child 66827 | c94531b5007d |

--- a/src/HOL/Analysis/Homeomorphism.thy Fri Sep 29 14:17:17 2017 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Fri Sep 29 16:55:08 2017 +0100 @@ -827,7 +827,7 @@ fixes a :: "'a :: euclidean_space" assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p" and aff: "aff_dim T = aff_dim p + 1" - shows "((sphere a r \<inter> T) - {b}) homeomorphic p" + shows "(sphere a r \<inter> T) - {b} homeomorphic p" proof - have "a \<noteq> b" using assms by auto then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))" @@ -847,6 +847,23 @@ finally show ?thesis . qed +corollary homeomorphic_punctured_sphere_affine: + fixes a :: "'a :: euclidean_space" + assumes "0 < r" and b: "b \<in> sphere a r" + and "affine T" and affS: "aff_dim T + 1 = DIM('a)" + shows "(sphere a r - {b}) homeomorphic T" + using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto + +corollary homeomorphic_punctured_sphere_hyperplane: + fixes a :: "'a :: euclidean_space" + assumes "0 < r" and b: "b \<in> sphere a r" + and "c \<noteq> 0" + shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}" +apply (rule homeomorphic_punctured_sphere_affine) +using assms +apply (auto simp: affine_hyperplane of_nat_diff) +done + proposition homeomorphic_punctured_sphere_affine_gen: fixes a :: "'a :: euclidean_space" assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S" @@ -892,24 +909,6 @@ finally show ?thesis . qed -corollary homeomorphic_punctured_sphere_affine: - fixes a :: "'a :: euclidean_space" - assumes "0 < r" and b: "b \<in> sphere a r" - and "affine T" and affS: "aff_dim T + 1 = DIM('a)" - shows "(sphere a r - {b}) homeomorphic T" -using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T] - assms aff_dim_cball by force - -corollary homeomorphic_punctured_sphere_hyperplane: - fixes a :: "'a :: euclidean_space" - assumes "0 < r" and b: "b \<in> sphere a r" - and "c \<noteq> 0" - shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}" -apply (rule homeomorphic_punctured_sphere_affine) -using assms -apply (auto simp: affine_hyperplane of_nat_diff) -done - text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set is homeomorphic to a closed subset of a convex set, and