equal
deleted
inserted
replaced
985 by (simp add: homeomorphic_translation) |
985 by (simp add: homeomorphic_translation) |
986 also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S" |
986 also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S" |
987 apply (simp add: homeomorphic_def homeomorphism_def) |
987 apply (simp add: homeomorphic_def homeomorphism_def) |
988 apply (rule_tac x="g \<circ> h" in exI) |
988 apply (rule_tac x="g \<circ> h" in exI) |
989 apply (rule_tac x="k \<circ> f" in exI) |
989 apply (rule_tac x="k \<circ> f" in exI) |
990 apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp) |
990 apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp) |
991 apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset) |
991 apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base) |
992 done |
992 done |
993 finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" . |
993 finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" . |
994 show ?thesis |
994 show ?thesis |
995 apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)" |
995 apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)" |
996 and T = "image (g o h) ((+) (- a) ` S)" |
996 and T = "image (g o h) ((+) (- a) ` S)" |