equal
deleted
inserted
replaced
1973 done |
1973 done |
1974 qed |
1974 qed |
1975 |
1975 |
1976 text \<open>So we get the no-retraction theorem.\<close> |
1976 text \<open>So we get the no-retraction theorem.\<close> |
1977 |
1977 |
1978 lemma no_retraction_cball: |
1978 theorem no_retraction_cball: |
1979 fixes a :: "'a::euclidean_space" |
1979 fixes a :: "'a::euclidean_space" |
1980 assumes "e > 0" |
1980 assumes "e > 0" |
1981 shows "\<not> (frontier (cball a e) retract_of (cball a e))" |
1981 shows "\<not> (frontier (cball a e) retract_of (cball a e))" |
1982 proof |
1982 proof |
1983 assume *: "frontier (cball a e) retract_of (cball a e)" |
1983 assume *: "frontier (cball a e) retract_of (cball a e)" |
1997 then have "a = x" |
1997 then have "a = x" |
1998 unfolding scaleR_left_distrib[symmetric] |
1998 unfolding scaleR_left_distrib[symmetric] |
1999 by auto |
1999 by auto |
2000 then show False |
2000 then show False |
2001 using x assms by auto |
2001 using x assms by auto |
|
2002 qed |
|
2003 |
|
2004 corollary contractible_sphere: |
|
2005 fixes a :: "'a::euclidean_space" |
|
2006 shows "contractible(sphere a r) \<longleftrightarrow> r \<le> 0" |
|
2007 proof (cases "0 < r") |
|
2008 case True |
|
2009 then show ?thesis |
|
2010 unfolding contractible_def nullhomotopic_from_sphere_extension |
|
2011 using no_retraction_cball [OF True, of a] |
|
2012 by (auto simp: retract_of_def retraction_def) |
|
2013 next |
|
2014 case False |
|
2015 then show ?thesis |
|
2016 unfolding contractible_def nullhomotopic_from_sphere_extension |
|
2017 apply (simp add: not_less) |
|
2018 apply (rule_tac x=id in exI) |
|
2019 apply (auto simp: continuous_on_def) |
|
2020 apply (meson dist_not_less_zero le_less less_le_trans) |
|
2021 done |
2002 qed |
2022 qed |
2003 |
2023 |
2004 subsection\<open>Retractions\<close> |
2024 subsection\<open>Retractions\<close> |
2005 |
2025 |
2006 lemma retraction: |
2026 lemma retraction: |