# HG changeset patch
# User huffman
# Date 1313452085 25200
# Node ID f0e442e248160c7e29c0514788d6f2144c8e7f01
# Parent  5cdad94bdc2906772b1cacc7662e1ef8480cb08a
add lemma tendsto_compose

diff -r 5cdad94bdc29 -r f0e442e24816 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Mon Aug 15 16:18:13 2011 -0700
+++ b/src/HOL/Lim.thy	Mon Aug 15 16:48:05 2011 -0700
@@ -252,26 +252,7 @@
   assumes g: "g -- l --> g l"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. g (f x)) -- a --> g l"
-proof (rule topological_tendstoI)
-  fix C assume C: "open C" "g l \<in> C"
-  obtain B where B: "open B" "l \<in> B"
-    and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> C"
-    using topological_tendstoD [OF g C]
-    unfolding eventually_at_topological by fast
-  obtain A where A: "open A" "a \<in> A"
-    and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
-    using topological_tendstoD [OF f B]
-    unfolding eventually_at_topological by fast
-  show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
-  unfolding eventually_at_topological
-  proof (intro exI conjI ballI impI)
-    show "open A" and "a \<in> A" using A .
-  next
-    fix x assume "x \<in> A" and "x \<noteq> a"
-    then show "g (f x) \<in> C"
-      by (cases "f x = l", simp add: C, simp add: gC fB)
-  qed
-qed
+  using assms by (rule tendsto_compose)
 
 lemma LIM_compose_eventually:
   assumes f: "f -- a --> b"
diff -r 5cdad94bdc29 -r f0e442e24816 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Aug 15 16:18:13 2011 -0700
+++ b/src/HOL/Limits.thy	Mon Aug 15 16:48:05 2011 -0700
@@ -611,6 +611,22 @@
   assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
   by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
 
+lemma tendsto_compose:
+  assumes g: "(g ---> g l) (at l)"
+  assumes f: "(f ---> l) F"
+  shows "((\<lambda>x. g (f x)) ---> g l) F"
+proof (rule topological_tendstoI)
+  fix B assume B: "open B" "g l \<in> B"
+  obtain A where A: "open A" "l \<in> A"
+    and gB: "\<forall>y. y \<in> A \<longrightarrow> g y \<in> B"
+    using topological_tendstoD [OF g B] B(2)
+    unfolding eventually_at_topological by fast
+  hence "\<forall>x. f x \<in> A \<longrightarrow> g (f x) \<in> B" by simp
+  from this topological_tendstoD [OF f A]
+  show "eventually (\<lambda>x. g (f x) \<in> B) F"
+    by (rule eventually_mono)
+qed
+
 subsubsection {* Distance and norms *}
 
 lemma tendsto_dist [tendsto_intros]: