--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:49 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 15:03:50 2013 -0700
@@ -1614,14 +1614,6 @@
qed
qed
-lemma Lim_inv: (* TODO: delete *)
- fixes f :: "'a \<Rightarrow> real"
- and A :: "'a filter"
- assumes "(f ---> l) A"
- and "l \<noteq> 0"
- shows "((inverse \<circ> f) ---> inverse l) A"
- unfolding o_def using assms by (rule tendsto_inverse)
-
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"