summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Homotopy.thy

changeset 69768 | 7e4966eaf781 |

parent 69712 | dc85b5b3a532 |

child 69918 | eddcc7c726f3 |

1.1 --- a/src/HOL/Analysis/Homotopy.thy Thu Jan 31 09:30:15 2019 +0100 1.2 +++ b/src/HOL/Analysis/Homotopy.thy Thu Jan 31 13:08:59 2019 +0000 1.3 @@ -3168,11 +3168,11 @@ 1.4 have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)" 1.5 using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def) 1.6 have "S homeomorphic ((+) (- a) ` S)" 1.7 - by (simp add: homeomorphic_translation) 1.8 + by (fact homeomorphic_translation) 1.9 also have "\<dots> homeomorphic ((+) (- b) ` T)" 1.10 by (rule homeomorphic_subspaces [OF ss dd]) 1.11 also have "\<dots> homeomorphic T" 1.12 - using homeomorphic_sym homeomorphic_translation by auto 1.13 + using homeomorphic_translation [of T "- b"] by (simp add: homeomorphic_sym [of T]) 1.14 finally show ?thesis . 1.15 qed 1.16