removed unused lemma
authorhuffman
Tue Sep 24 15:03:50 2013 -0700 (2013-09-24)
changeset 538615ba90fca32bc
parent 53860 f2d683432580
child 53862 cb1094587ee4
removed unused lemma
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:49 2013 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 15:03:50 2013 -0700
     1.3 @@ -1614,14 +1614,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma Lim_inv: (* TODO: delete *)
     1.8 -  fixes f :: "'a \<Rightarrow> real"
     1.9 -    and A :: "'a filter"
    1.10 -  assumes "(f ---> l) A"
    1.11 -    and "l \<noteq> 0"
    1.12 -  shows "((inverse \<circ> f) ---> inverse l) A"
    1.13 -  unfolding o_def using assms by (rule tendsto_inverse)
    1.14 -
    1.15  lemma Lim_null:
    1.16    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.17    shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"