95 fixes S :: "'a :: {heine_borel,real_normed_vector} set" |
95 fixes S :: "'a :: {heine_borel,real_normed_vector} set" |
96 shows "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T" |
96 shows "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T" |
97 by (metis locally_compact_closedin closedin_retract) |
97 by (metis locally_compact_closedin closedin_retract) |
98 |
98 |
99 lemma homotopic_into_retract: |
99 lemma homotopic_into_retract: |
100 "\<lbrakk>f \<in> S \<rightarrow> T; g \<in> S \<rightarrow> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk> |
100 assumes fg: "f \<in> S \<rightarrow> T" "g \<in> S \<rightarrow> T" |
101 \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g" |
101 assumes "T retract_of U" |
102 apply (subst (asm) homotopic_with_def) |
102 assumes "homotopic_with_canon (\<lambda>x. True) S U f g" |
103 apply (simp add: homotopic_with retract_of_def retraction_def Pi_iff, clarify) |
103 shows "homotopic_with_canon (\<lambda>x. True) S T f g" |
104 apply (rule_tac x="r \<circ> h" in exI) |
104 proof - |
105 by (smt (verit, ccfv_SIG) comp_def continuous_on_compose continuous_on_subset image_subset_iff) |
105 obtain h r where r: "retraction U T r" |
|
106 "continuous_on ({0..1::real} \<times> S) h" |
|
107 and h: "h \<in> {0..1} \<times> S \<rightarrow> U \<and> (\<forall>x. h (0, x) = f x) \<and> (\<forall>x. h (1, x) = g x)" |
|
108 using assms by (auto simp: homotopic_with_def retract_of_def) |
|
109 then have "continuous_on ({0..1} \<times> S) (r \<circ> h)" |
|
110 by (metis continuous_on_compose continuous_on_subset funcset_image |
|
111 retraction_def) |
|
112 then show ?thesis |
|
113 using r fg h |
|
114 apply (simp add: retraction homotopic_with Pi_iff) |
|
115 by (smt (verit, best) imageI) |
|
116 qed |
106 |
117 |
107 lemma retract_of_locally_connected: |
118 lemma retract_of_locally_connected: |
108 assumes "locally connected T" "S retract_of T" |
119 assumes "locally connected T" "S retract_of T" |
109 shows "locally connected S" |
120 shows "locally connected S" |
110 using assms |
121 using assms |
129 using r unfolding retraction_def |
140 using r unfolding retraction_def |
130 by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology) |
141 by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology) |
131 ultimately |
142 ultimately |
132 show ?thesis |
143 show ?thesis |
133 unfolding homotopy_equivalent_space_def |
144 unfolding homotopy_equivalent_space_def |
134 by (smt (verit, del_insts) continuous_map_id continuous_map_subtopology_eu id_def r retraction retraction_comp subset_refl) |
145 by (meson continuous_map_from_subtopology_mono continuous_map_id |
|
146 continuous_map_subtopology_eu r retraction_def) |
135 qed |
147 qed |
136 |
148 |
137 lemma deformation_retract: |
149 lemma deformation_retract: |
138 fixes S :: "'a::euclidean_space set" |
150 fixes S :: "'a::euclidean_space set" |
139 shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow> |
151 shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow> |
2233 using assms by (auto simp: path_component_def) |
2245 using assms by (auto simp: path_component_def) |
2234 define h where "h \<equiv> \<lambda>z. (snd z - (g \<circ> fst) z) /\<^sub>R norm (snd z - (g \<circ> fst) z)" |
2246 define h where "h \<equiv> \<lambda>z. (snd z - (g \<circ> fst) z) /\<^sub>R norm (snd z - (g \<circ> fst) z)" |
2235 have "continuous_on ({0..1} \<times> S) h" |
2247 have "continuous_on ({0..1} \<times> S) h" |
2236 unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs) |
2248 unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs) |
2237 moreover |
2249 moreover |
2238 have "h ` ({0..1} \<times> S) \<subseteq> sphere 0 1" |
2250 have "h \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1" |
2239 unfolding h_def using g by (auto simp: divide_simps path_defs) |
2251 unfolding h_def using g by (auto simp: divide_simps path_defs) |
2240 ultimately show ?thesis |
2252 ultimately show ?thesis |
2241 using g by (auto simp: h_def path_defs homotopic_with_def) |
2253 using g by (auto simp: h_def path_defs homotopic_with_def) |
2242 qed |
2254 qed |
2243 |
2255 |