equal
deleted
inserted
replaced
82 apply (rule Retracts.homotopically_trivial_retraction_null_gen) |
82 apply (rule Retracts.homotopically_trivial_retraction_null_gen) |
83 apply (rule TrueI refl assms that | assumption)+ |
83 apply (rule TrueI refl assms that | assumption)+ |
84 done |
84 done |
85 qed |
85 qed |
86 |
86 |
87 lemma retraction_imp_quotient_map: |
87 lemma retraction_openin_vimage_iff: |
88 "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" |
88 "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U" |
89 if retraction: "retraction S T r" and "U \<subseteq> T" |
89 if retraction: "retraction S T r" and "U \<subseteq> T" |
90 using retraction apply (rule retractionE) |
90 using retraction apply (rule retractionE) |
91 apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) |
91 apply (rule continuous_right_inverse_imp_quotient_map [where g=r]) |
92 using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset) |
92 using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset) |
108 |
108 |
109 lemma retract_of_locally_connected: |
109 lemma retract_of_locally_connected: |
110 assumes "locally connected T" "S retract_of T" |
110 assumes "locally connected T" "S retract_of T" |
111 shows "locally connected S" |
111 shows "locally connected S" |
112 using assms |
112 using assms |
113 by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE) |
113 by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE) |
114 |
114 |
115 lemma retract_of_locally_path_connected: |
115 lemma retract_of_locally_path_connected: |
116 assumes "locally path_connected T" "S retract_of T" |
116 assumes "locally path_connected T" "S retract_of T" |
117 shows "locally path_connected S" |
117 shows "locally path_connected S" |
118 using assms |
118 using assms |
119 by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE) |
119 by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE) |
120 |
120 |
121 text \<open>A few simple lemmas about deformation retracts\<close> |
121 text \<open>A few simple lemmas about deformation retracts\<close> |
122 |
122 |
123 lemma deformation_retract_imp_homotopy_eqv: |
123 lemma deformation_retract_imp_homotopy_eqv: |
124 fixes S :: "'a::euclidean_space set" |
124 fixes S :: "'a::euclidean_space set" |