src/HOL/Real_Vector_Spaces.thy
changeset 61969 e01015e49041
parent 61942 f02b26f7d39d
child 61973 0c7e865fa7cb
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 29 22:41:22 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Dec 29 23:04:53 2015 +0100
     1.3 @@ -1708,20 +1708,20 @@
     1.4  
     1.5  subsubsection \<open>Limits of Sequences\<close>
     1.6  
     1.7 -lemma lim_sequentially: "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 \<longlonglongrightarrow> (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  lemmas LIMSEQ_def = lim_sequentially  (*legacy binding*)
    1.12  
    1.13 -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.14 +lemma LIMSEQ_iff_nz: "X \<longlonglongrightarrow> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    1.15    unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
    1.16  
    1.17  lemma metric_LIMSEQ_I:
    1.18 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
    1.19 +  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X \<longlonglongrightarrow> (L::'a::metric_space)"
    1.20  by (simp add: lim_sequentially)
    1.21  
    1.22  lemma metric_LIMSEQ_D:
    1.23 -  "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
    1.24 +  "\<lbrakk>X \<longlonglongrightarrow> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
    1.25  by (simp add: lim_sequentially)
    1.26  
    1.27  
    1.28 @@ -1840,7 +1840,7 @@
    1.29  done
    1.30  
    1.31  theorem LIMSEQ_imp_Cauchy:
    1.32 -  assumes X: "X ----> a" shows "Cauchy X"
    1.33 +  assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
    1.34  proof (rule metric_CauchyI)
    1.35    fix e::real assume "0 < e"
    1.36    hence "0 < e/2" by simp
    1.37 @@ -1890,7 +1890,7 @@
    1.38    assumes inc: "\<And>n. f n \<le> f (Suc n)"
    1.39        and bdd: "\<And>n. f n \<le> l"
    1.40        and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
    1.41 -  shows "f ----> l"
    1.42 +  shows "f \<longlonglongrightarrow> l"
    1.43  proof (rule increasing_tendsto)
    1.44    fix x assume "x < l"
    1.45    with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
    1.46 @@ -1937,7 +1937,7 @@
    1.47      thus "\<And>s. s \<in> S \<Longrightarrow>  s \<le> X N + 1"
    1.48        by (rule bound_isUb)
    1.49    qed
    1.50 -  have "X ----> Sup S"
    1.51 +  have "X \<longlonglongrightarrow> Sup S"
    1.52    proof (rule metric_LIMSEQ_I)
    1.53    fix r::real assume "0 < r"
    1.54    hence r: "0 < r/2" by simp
    1.55 @@ -1976,7 +1976,7 @@
    1.56  
    1.57  lemma tendsto_at_topI_sequentially:
    1.58    fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
    1.59 -  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
    1.60 +  assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
    1.61    shows "(f ---> y) at_top"
    1.62  proof -
    1.63    from nhds_countable[of y] guess A . note A = this
    1.64 @@ -2008,7 +2008,7 @@
    1.65  lemma tendsto_at_topI_sequentially_real:
    1.66    fixes f :: "real \<Rightarrow> real"
    1.67    assumes mono: "mono f"
    1.68 -  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
    1.69 +  assumes limseq: "(\<lambda>n. f (real n)) \<longlonglongrightarrow> y"
    1.70    shows "(f ---> y) at_top"
    1.71  proof (rule tendstoI)
    1.72    fix e :: real assume "0 < e"