# 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