src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 64006 0de4736dad8b
parent 63928 d81fb5b46a5c
child 64122 74fde524799e
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Oct 02 21:05:14 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Oct 03 13:01:01 2016 +0100
     1.3 @@ -1975,7 +1975,7 @@
     1.4  
     1.5  text \<open>So we get the no-retraction theorem.\<close>
     1.6  
     1.7 -lemma no_retraction_cball:
     1.8 +theorem no_retraction_cball:
     1.9    fixes a :: "'a::euclidean_space"
    1.10    assumes "e > 0"
    1.11    shows "\<not> (frontier (cball a e) retract_of (cball a e))"
    1.12 @@ -2001,6 +2001,26 @@
    1.13      using x assms by auto
    1.14  qed
    1.15  
    1.16 +corollary contractible_sphere:
    1.17 +  fixes a :: "'a::euclidean_space"
    1.18 +  shows "contractible(sphere a r) \<longleftrightarrow> r \<le> 0"
    1.19 +proof (cases "0 < r")
    1.20 +  case True
    1.21 +  then show ?thesis
    1.22 +    unfolding contractible_def nullhomotopic_from_sphere_extension
    1.23 +    using no_retraction_cball [OF True, of a]
    1.24 +    by (auto simp: retract_of_def retraction_def)
    1.25 +next
    1.26 +  case False
    1.27 +  then show ?thesis
    1.28 +    unfolding contractible_def nullhomotopic_from_sphere_extension
    1.29 +    apply (simp add: not_less)
    1.30 +    apply (rule_tac x=id in exI)
    1.31 +    apply (auto simp: continuous_on_def)
    1.32 +    apply (meson dist_not_less_zero le_less less_le_trans)
    1.33 +    done
    1.34 +qed
    1.35 +
    1.36  subsection\<open>Retractions\<close>
    1.37  
    1.38  lemma retraction: