src/HOL/Real_Vector_Spaces.thy
 changeset 60017 b785d6d06430 parent 59867 58043346ca64 child 60026 41d81b4a0a21
```--- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Apr 11 11:56:40 2015 +0100
@@ -1544,19 +1544,19 @@

subsubsection {* Limits of Sequences *}

-lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
unfolding tendsto_iff eventually_sequentially ..

lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
-  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
+  unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)

lemma metric_LIMSEQ_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"

lemma metric_LIMSEQ_D:
"\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"