# HG changeset patch
# User huffman
# Date 1380060230 25200
# Node ID 5ba90fca32bc3217c5b710ab5d2c63753010213f
# Parent  f2d6834325806391cfbc1bd34980115dc0405cb6
removed unused lemma

diff -r f2d683432580 -r 5ba90fca32bc src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"