src/HOL/Analysis/Homeomorphism.thy

 
 theorem homeomorphic_punctured_affine_sphere_affine:
   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))"
     by (simp add: inj_on_def)
   have "((sphere a r \<inter> T) - {b}) homeomorphic

     using assms
     apply (auto simp: dist_norm norm_minus_commute affine_scaling affine_translation [symmetric] aff_dim_translation_eq inj)
     done
   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"
       and "affine T" and affS: "aff_dim S = aff_dim T + 1"

     apply (rule homeomorphic_punctured_affine_sphere_affine)
     using a him
     by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>)
   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
   if the set is locally compact we can take the convex set to be the universe.\<close>