eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
authorpaulson <lp15@cam.ac.uk>
Fri Sep 29 16:55:08 2017 +0100 (18 months ago)
changeset 66710676258a1cf01
parent 66709 b034d2ae541c
child 66723 18cc87e2335f
eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
src/HOL/Analysis/Homeomorphism.thy
     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