src/HOL/Real_Vector_Spaces.thy
changeset 60017 b785d6d06430
parent 59867 58043346ca64
child 60026 41d81b4a0a21
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -1544,19 +1544,19 @@
     1.4  
     1.5  subsubsection {* Limits of Sequences *}
     1.6  
     1.7 -lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
     1.8 +lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
     1.9    unfolding tendsto_iff eventually_sequentially ..
    1.10  
    1.11  lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    1.12 -  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
    1.13 +  unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
    1.14  
    1.15  lemma metric_LIMSEQ_I:
    1.16    "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
    1.17 -by (simp add: LIMSEQ_def)
    1.18 +by (simp add: lim_sequentially)
    1.19  
    1.20  lemma metric_LIMSEQ_D:
    1.21    "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
    1.22 -by (simp add: LIMSEQ_def)
    1.23 +by (simp add: lim_sequentially)
    1.24  
    1.25  
    1.26  subsubsection {* Limits of Functions *}
    1.27 @@ -1823,7 +1823,7 @@
    1.28  proof (rule tendstoI)
    1.29    fix e :: real assume "0 < e"
    1.30    with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
    1.31 -    by (auto simp: LIMSEQ_def dist_real_def)
    1.32 +    by (auto simp: lim_sequentially dist_real_def)
    1.33    { fix x :: real
    1.34      obtain n where "x \<le> real_of_nat n"
    1.35        using ex_le_of_nat[of x] ..