Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove trivial lemma Lim_at_iff_LIM
authorhuffman
Mon, 12 Sep 2011 10:43:36 -0700
changeset 44905 3e8cc9046731
parent 44904 2ba4174f1e7d
child 44906 8f3625167c76
remove trivial lemma Lim_at_iff_LIM
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle