# HG changeset patch # User paulson # Date 1506700508 -3600 # Node ID 676258a1cf01efab9d9755d361594637ceb7ee12 # Parent b034d2ae541c637187226316fd66bae7586a3a6e eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen diff -r b034d2ae541c -r 676258a1cf01 src/HOL/Analysis/Homeomorphism.thy --- 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 \ sphere a r" "affine T" "a \ T" "b \ T" "affine p" and aff: "aff_dim T = aff_dim p + 1" - shows "((sphere a r \ T) - {b}) homeomorphic p" + shows "(sphere a r \ T) - {b} homeomorphic p" proof - have "a \ b" using assms by auto then have inj: "inj (\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 \ 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 \ sphere a r" + and "c \ 0" + shows "(sphere a r - {b}) homeomorphic {x::'a. c \ 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 \ 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 \ 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 \ sphere a r" - and "c \ 0" - shows "(sphere a r - {b}) homeomorphic {x::'a. c \ x = d}" -apply (rule homeomorphic_punctured_sphere_affine) -using assms -apply (auto simp: affine_hyperplane of_nat_diff) -done - text\ 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