# HG changeset patch
# User huffman
# Date 1394819983 25200
# Node ID 30bbc100d6900462a5c63dee54641ae854506450
# Parent  ede82d6e0abdbde8cd1bb1cd3ee77c2a3980ccc3
remove unused lemma which was a direct consequence of tendsto_intros

diff -r ede82d6e0abd -r 30bbc100d690 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 14 19:15:50 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 14 10:59:43 2014 -0700
@@ -293,20 +293,6 @@
 
 subsection {* Differentiability implies continuity *}
 
-lemma Lim_mul_norm_within:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f x) ---> 0) (at a within s)"
-  unfolding Lim_within
-  apply (auto simp: )
-  apply (erule_tac x=e in allE)
-  apply (auto simp: )
-  apply (rule_tac x="min d 1" in exI)
-  apply (auto simp: )
-  apply (erule_tac x=x in ballE)
-  unfolding dist_norm diff_0_right
-  apply (auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
-  done
-
 lemma differentiable_imp_continuous_within:
   "f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (auto simp: differentiable_def intro: FDERIV_continuous)