250 |
250 |
251 lemma LIM_compose: |
251 lemma LIM_compose: |
252 assumes g: "g -- l --> g l" |
252 assumes g: "g -- l --> g l" |
253 assumes f: "f -- a --> l" |
253 assumes f: "f -- a --> l" |
254 shows "(\<lambda>x. g (f x)) -- a --> g l" |
254 shows "(\<lambda>x. g (f x)) -- a --> g l" |
255 proof (rule topological_tendstoI) |
255 using assms by (rule tendsto_compose) |
256 fix C assume C: "open C" "g l \<in> C" |
|
257 obtain B where B: "open B" "l \<in> B" |
|
258 and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C" |
|
259 using topological_tendstoD [OF g C] |
|
260 unfolding eventually_at_topological by fast |
|
261 obtain A where A: "open A" "a \<in> A" |
|
262 and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B" |
|
263 using topological_tendstoD [OF f B] |
|
264 unfolding eventually_at_topological by fast |
|
265 show "eventually (\<lambda>x. g (f x) \<in> C) (at a)" |
|
266 unfolding eventually_at_topological |
|
267 proof (intro exI conjI ballI impI) |
|
268 show "open A" and "a \<in> A" using A . |
|
269 next |
|
270 fix x assume "x \<in> A" and "x \<noteq> a" |
|
271 then show "g (f x) \<in> C" |
|
272 by (cases "f x = l", simp add: C, simp add: gC fB) |
|
273 qed |
|
274 qed |
|
275 |
256 |
276 lemma LIM_compose_eventually: |
257 lemma LIM_compose_eventually: |
277 assumes f: "f -- a --> b" |
258 assumes f: "f -- a --> b" |
278 assumes g: "g -- b --> c" |
259 assumes g: "g -- b --> c" |
279 assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" |
260 assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)" |