# HG changeset patch
# User huffman
# Date 1315849416 25200
# Node ID 3e8cc9046731598a8c499c3a93b8791f310276cf
# Parent  2ba4174f1e7d28cdf56474d78eb0e1ab5876c0cc
remove trivial lemma Lim_at_iff_LIM

diff -r 2ba4174f1e7d -r 3e8cc9046731 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 10:28:45 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 10:43:36 2011 -0700
@@ -963,9 +963,6 @@
         (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at)
 
-lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
-  unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
-
 lemma Lim_at_infinity:
   "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at_infinity)