Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
authorpaulson <lp15@cam.ac.uk>
Mon Sep 25 15:49:27 2017 +0100 (19 months ago)
changeset 666906953b1a29e19
parent 66689 ef81649ad051
child 66691 a8703e8ee1d3
child 66708 015a95f15040
Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
src/HOL/Analysis/Homeomorphism.thy
     1.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 25 09:46:26 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 25 15:49:27 2017 +0100
     1.3 @@ -853,19 +853,15 @@
     1.4        and "affine T" and affS: "aff_dim S = aff_dim T + 1"
     1.5      shows "rel_frontier S - {a} homeomorphic T"
     1.6  proof -
     1.7 -  have "S \<noteq> {}" using assms by auto
     1.8 -  obtain U :: "'a set" where "affine U" and affdS: "aff_dim U = aff_dim S"
     1.9 +  obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
    1.10      using choose_affine_subset [OF affine_UNIV aff_dim_geq]
    1.11 -    by (meson aff_dim_affine_hull affine_affine_hull)
    1.12 -  have "convex U"
    1.13 -    by (simp add: affine_imp_convex \<open>affine U\<close>)
    1.14 -  have "U \<noteq> {}"
    1.15 -    by (metis \<open>S \<noteq> {}\<close> \<open>aff_dim U = aff_dim S\<close> aff_dim_empty)
    1.16 +    by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
    1.17 +  have "S \<noteq> {}" using assms by auto
    1.18    then obtain z where "z \<in> U"
    1.19 -    by auto
    1.20 +    by (metis aff_dim_negative_iff equals0I affdS)
    1.21    then have bne: "ball z 1 \<inter> U \<noteq> {}" by force
    1.22 -  have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U"
    1.23 -    using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball] bne
    1.24 +  then have [simp]: "aff_dim(ball z 1 \<inter> U) = aff_dim U"
    1.25 +    using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball]
    1.26      by (fastforce simp add: Int_commute)
    1.27    have "rel_frontier S homeomorphic rel_frontier (ball z 1 \<inter> U)"
    1.28      apply (rule homeomorphic_rel_frontiers_convex_bounded_sets)
    1.29 @@ -874,7 +870,8 @@
    1.30    also have "... = sphere z 1 \<inter> U"
    1.31      using convex_affine_rel_frontier_Int [of "ball z 1" U]
    1.32      by (simp add: \<open>affine U\<close> bne)
    1.33 -  finally obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U"
    1.34 +  finally have "rel_frontier S homeomorphic sphere z 1 \<inter> U" . 
    1.35 +  then obtain h k where him: "h ` rel_frontier S = sphere z 1 \<inter> U"
    1.36                      and kim: "k ` (sphere z 1 \<inter> U) = rel_frontier S"
    1.37                      and hcon: "continuous_on (rel_frontier S) h"
    1.38                      and kcon: "continuous_on (sphere z 1 \<inter> U) k"
    1.39 @@ -882,7 +879,7 @@
    1.40                      and hk:  "\<And>y. y \<in> sphere z 1 \<inter> U \<Longrightarrow> h(k(y)) = y"
    1.41      unfolding homeomorphic_def homeomorphism_def by auto
    1.42    have "rel_frontier S - {a} homeomorphic (sphere z 1 \<inter> U) - {h a}"
    1.43 -  proof (rule homeomorphicI [where f=h and g=k])
    1.44 +  proof (rule homeomorphicI)
    1.45      show h: "h ` (rel_frontier S - {a}) = sphere z 1 \<inter> U - {h a}"
    1.46        using him a kh by auto metis
    1.47      show "k ` (sphere z 1 \<inter> U - {h a}) = rel_frontier S - {a}"
    1.48 @@ -891,12 +888,11 @@
    1.49    also have "... homeomorphic T"
    1.50      apply (rule homeomorphic_punctured_affine_sphere_affine)
    1.51      using a him
    1.52 -    by (auto simp: affS affdS \<open>affine T\<close>  \<open>affine U\<close> \<open>z \<in> U\<close>)
    1.53 +    by (auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>)
    1.54    finally show ?thesis .
    1.55  qed
    1.56  
    1.57 -
    1.58 -lemma homeomorphic_punctured_sphere_affine:
    1.59 +corollary homeomorphic_punctured_sphere_affine:
    1.60    fixes a :: "'a :: euclidean_space"
    1.61    assumes "0 < r" and b: "b \<in> sphere a r"
    1.62        and "affine T" and affS: "aff_dim T + 1 = DIM('a)"