author | paulson <lp15@cam.ac.uk> |

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