src/HOL/Limits.thy
changeset 44253 c073a0bd8458
parent 44251 d101ed3177b6
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/Limits.thy	Wed Aug 17 11:07:32 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Wed Aug 17 11:39:09 2011 -0700
     1.3 @@ -627,6 +627,22 @@
     1.4      by (rule eventually_mono)
     1.5  qed
     1.6  
     1.7 +lemma tendsto_compose_eventually:
     1.8 +  assumes g: "(g ---> m) (at l)"
     1.9 +  assumes f: "(f ---> l) F"
    1.10 +  assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
    1.11 +  shows "((\<lambda>x. g (f x)) ---> m) F"
    1.12 +proof (rule topological_tendstoI)
    1.13 +  fix B assume B: "open B" "m \<in> B"
    1.14 +  obtain A where A: "open A" "l \<in> A"
    1.15 +    and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B"
    1.16 +    using topological_tendstoD [OF g B]
    1.17 +    unfolding eventually_at_topological by fast
    1.18 +  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    1.19 +    using topological_tendstoD [OF f A] inj
    1.20 +    by (rule eventually_elim2) (simp add: gB)
    1.21 +qed
    1.22 +
    1.23  lemma metric_tendsto_imp_tendsto:
    1.24    assumes f: "(f ---> a) F"
    1.25    assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"