src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44905 3e8cc9046731
parent 44890 22f665a2e91c
child 44907 93943da0a010
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 10:28:45 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 10:43:36 2011 -0700
     1.3 @@ -963,9 +963,6 @@
     1.4          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
     1.5    by (auto simp add: tendsto_iff eventually_at)
     1.6  
     1.7 -lemma Lim_at_iff_LIM: "(f ---> l) (at a) \<longleftrightarrow> f -- a --> l"
     1.8 -  unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
     1.9 -
    1.10  lemma Lim_at_infinity:
    1.11    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
    1.12    by (auto simp add: tendsto_iff eventually_at_infinity)