add lemma tendsto_compose
authorhuffman
Mon Aug 15 16:48:05 2011 -0700 (2011-08-15)
changeset 44218f0e442e24816
parent 44217 5cdad94bdc29
child 44219 f738e3200e24
add lemma tendsto_compose
src/HOL/Lim.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Lim.thy	Mon Aug 15 16:18:13 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Mon Aug 15 16:48:05 2011 -0700
     1.3 @@ -252,26 +252,7 @@
     1.4    assumes g: "g -- l --> g l"
     1.5    assumes f: "f -- a --> l"
     1.6    shows "(\<lambda>x. g (f x)) -- a --> g l"
     1.7 -proof (rule topological_tendstoI)
     1.8 -  fix C assume C: "open C" "g l \<in> C"
     1.9 -  obtain B where B: "open B" "l \<in> B"
    1.10 -    and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C"
    1.11 -    using topological_tendstoD [OF g C]
    1.12 -    unfolding eventually_at_topological by fast
    1.13 -  obtain A where A: "open A" "a \<in> A"
    1.14 -    and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
    1.15 -    using topological_tendstoD [OF f B]
    1.16 -    unfolding eventually_at_topological by fast
    1.17 -  show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
    1.18 -  unfolding eventually_at_topological
    1.19 -  proof (intro exI conjI ballI impI)
    1.20 -    show "open A" and "a \<in> A" using A .
    1.21 -  next
    1.22 -    fix x assume "x \<in> A" and "x \<noteq> a"
    1.23 -    then show "g (f x) \<in> C"
    1.24 -      by (cases "f x = l", simp add: C, simp add: gC fB)
    1.25 -  qed
    1.26 -qed
    1.27 +  using assms by (rule tendsto_compose)
    1.28  
    1.29  lemma LIM_compose_eventually:
    1.30    assumes f: "f -- a --> b"
     2.1 --- a/src/HOL/Limits.thy	Mon Aug 15 16:18:13 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Mon Aug 15 16:48:05 2011 -0700
     2.3 @@ -611,6 +611,22 @@
     2.4    assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
     2.5    by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
     2.6  
     2.7 +lemma tendsto_compose:
     2.8 +  assumes g: "(g ---> g l) (at l)"
     2.9 +  assumes f: "(f ---> l) F"
    2.10 +  shows "((\<lambda>x. g (f x)) ---> g l) F"
    2.11 +proof (rule topological_tendstoI)
    2.12 +  fix B assume B: "open B" "g l \<in> B"
    2.13 +  obtain A where A: "open A" "l \<in> A"
    2.14 +    and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B"
    2.15 +    using topological_tendstoD [OF g B] B(2)
    2.16 +    unfolding eventually_at_topological by fast
    2.17 +  hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp
    2.18 +  from this topological_tendstoD [OF f A]
    2.19 +  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    2.20 +    by (rule eventually_mono)
    2.21 +qed
    2.22 +
    2.23  subsubsection {* Distance and norms *}
    2.24  
    2.25  lemma tendsto_dist [tendsto_intros]: