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:
```