src/HOL/SEQ.thy
changeset 33271 7be66dee1a5a
parent 33042 ddf1f03a9ad9
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/SEQ.thy	Tue Oct 27 14:46:03 2009 +0000
     1.2 +++ b/src/HOL/SEQ.thy	Wed Oct 28 11:42:31 2009 +0000
     1.3 @@ -205,6 +205,9 @@
     1.4    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
     1.5  unfolding LIMSEQ_def dist_norm ..
     1.6  
     1.7 +lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
     1.8 +  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
     1.9 +
    1.10  lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
    1.11  by (simp only: LIMSEQ_iff Zseq_def)
    1.12