# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1396453531 -3600
# Node ID 0362c3bb4d02243c7d5ec70c07087f15eb3e4908
# Parent  713f9b9a7e51fa46a5de698ddd2611dbde7fa083
new theorem about zero limits

diff -r 713f9b9a7e51 -r 0362c3bb4d02 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Apr 02 16:34:37 2014 +0100
+++ b/src/HOL/Limits.thy	Wed Apr 02 16:45:31 2014 +0100
@@ -404,6 +404,10 @@
 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
   by (simp only: tendsto_iff Zfun_def dist_norm)
 
+lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk> 
+                     \<Longrightarrow> (g ---> 0) F"
+  by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
+
 subsubsection {* Distance and norms *}
 
 lemma tendsto_dist [tendsto_intros]: