equal
deleted
inserted
replaced
147 then show ?lhs |
147 then show ?lhs |
148 apply (clarsimp simp add: retract_of_def retraction_def) |
148 apply (clarsimp simp add: retract_of_def retraction_def) |
149 apply (rule_tac x=r in exI, simp) |
149 apply (rule_tac x=r in exI, simp) |
150 apply (rule homotopic_with_trans, assumption) |
150 apply (rule homotopic_with_trans, assumption) |
151 apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq) |
151 apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq) |
152 apply (rule_tac Y=S in homotopic_compose_continuous_left) |
152 apply (rule_tac Y=S in homotopic_with_compose_continuous_left) |
153 apply (auto simp: homotopic_with_sym) |
153 apply (auto simp: homotopic_with_sym) |
154 done |
154 done |
155 qed |
155 qed |
156 |
156 |
157 lemma deformation_retract_of_contractible_sing: |
157 lemma deformation_retract_of_contractible_sing: |