remove redundant lemma
authorhuffman
Wed Aug 10 15:56:48 2011 -0700 (2011-08-10)
changeset 44139abccf1b7ea4b
parent 44138 0c9feac80852
child 44140 2c10c35dd4be
remove redundant lemma
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 14:25:56 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 15:56:48 2011 -0700
     1.3 @@ -1031,9 +1031,6 @@
     1.4            (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)"
     1.5    by (auto simp add: tendsto_iff eventually_sequentially)
     1.6  
     1.7 -lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
     1.8 -  unfolding Lim_sequentially LIMSEQ_def ..
     1.9 -
    1.10  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    1.11    by (rule topological_tendstoI, auto elim: eventually_rev_mono)
    1.12