equal
deleted
inserted
replaced
4180 apply (rule assms(6)[rule_format]) |
4180 apply (rule assms(6)[rule_format]) |
4181 apply rule |
4181 apply rule |
4182 apply (rule continuous_on_compose assms)+ |
4182 apply (rule continuous_on_compose assms)+ |
4183 apply ((rule continuous_on_subset)?, rule assms)+ |
4183 apply ((rule continuous_on_subset)?, rule assms)+ |
4184 using assms(2,4,8) |
4184 using assms(2,4,8) |
4185 unfolding image_compose |
|
4186 apply auto |
4185 apply auto |
4187 apply blast |
4186 apply blast |
4188 done |
4187 done |
4189 then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" .. |
4188 then obtain x where x: "x \<in> s" "(i \<circ> g \<circ> r) x = x" .. |
4190 then have *: "g (r x) \<in> t" |
4189 then have *: "g (r x) \<in> t" |