author paulson Fri Sep 29 16:55:08 2017 +0100 (21 months ago) changeset 66710 676258a1cf01 parent 66709 b034d2ae541c child 66723 18cc87e2335f
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
```     1.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Fri Sep 29 14:17:17 2017 +0100
1.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Fri Sep 29 16:55:08 2017 +0100
1.3 @@ -827,7 +827,7 @@
1.4    fixes a :: "'a :: euclidean_space"
1.5    assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
1.6        and aff: "aff_dim T = aff_dim p + 1"
1.7 -    shows "((sphere a r \<inter> T) - {b}) homeomorphic p"
1.8 +    shows "(sphere a r \<inter> T) - {b} homeomorphic p"
1.9  proof -
1.10    have "a \<noteq> b" using assms by auto
1.11    then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
1.12 @@ -847,6 +847,23 @@
1.13    finally show ?thesis .
1.14  qed
1.15
1.16 +corollary homeomorphic_punctured_sphere_affine:
1.17 +  fixes a :: "'a :: euclidean_space"
1.18 +  assumes "0 < r" and b: "b \<in> sphere a r"
1.19 +      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
1.20 +    shows "(sphere a r - {b}) homeomorphic T"
1.21 +  using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto
1.22 +
1.23 +corollary homeomorphic_punctured_sphere_hyperplane:
1.24 +  fixes a :: "'a :: euclidean_space"
1.25 +  assumes "0 < r" and b: "b \<in> sphere a r"
1.26 +      and "c \<noteq> 0"
1.27 +    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
1.28 +apply (rule homeomorphic_punctured_sphere_affine)
1.29 +using assms
1.30 +apply (auto simp: affine_hyperplane of_nat_diff)
1.31 +done
1.32 +
1.33  proposition homeomorphic_punctured_sphere_affine_gen:
1.34    fixes a :: "'a :: euclidean_space"
1.35    assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
1.36 @@ -892,24 +909,6 @@
1.37    finally show ?thesis .
1.38  qed
1.39
1.40 -corollary homeomorphic_punctured_sphere_affine:
1.41 -  fixes a :: "'a :: euclidean_space"
1.42 -  assumes "0 < r" and b: "b \<in> sphere a r"
1.43 -      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
1.44 -    shows "(sphere a r - {b}) homeomorphic T"
1.45 -using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T]
1.46 -  assms aff_dim_cball by force
1.47 -
1.48 -corollary homeomorphic_punctured_sphere_hyperplane:
1.49 -  fixes a :: "'a :: euclidean_space"
1.50 -  assumes "0 < r" and b: "b \<in> sphere a r"
1.51 -      and "c \<noteq> 0"
1.52 -    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
1.53 -apply (rule homeomorphic_punctured_sphere_affine)
1.54 -using assms
1.55 -apply (auto simp: affine_hyperplane of_nat_diff)
1.56 -done
1.57 -
1.58
1.59  text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
1.60    is homeomorphic to a closed subset of a convex set, and
```