src/HOL/Limits.thy
changeset 44218 f0e442e24816
parent 44206 5e4a1664106e
child 44251 d101ed3177b6
     1.1 --- a/src/HOL/Limits.thy	Mon Aug 15 16:18:13 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Mon Aug 15 16:48:05 2011 -0700
     1.3 @@ -611,6 +611,22 @@
     1.4    assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
     1.5    by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
     1.6  
     1.7 +lemma tendsto_compose:
     1.8 +  assumes g: "(g ---> g l) (at l)"
     1.9 +  assumes f: "(f ---> l) F"
    1.10 +  shows "((\<lambda>x. g (f x)) ---> g l) F"
    1.11 +proof (rule topological_tendstoI)
    1.12 +  fix B assume B: "open B" "g l \<in> B"
    1.13 +  obtain A where A: "open A" "l \<in> A"
    1.14 +    and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B"
    1.15 +    using topological_tendstoD [OF g B] B(2)
    1.16 +    unfolding eventually_at_topological by fast
    1.17 +  hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp
    1.18 +  from this topological_tendstoD [OF f A]
    1.19 +  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    1.20 +    by (rule eventually_mono)
    1.21 +qed
    1.22 +
    1.23  subsubsection {* Distance and norms *}
    1.24  
    1.25  lemma tendsto_dist [tendsto_intros]: