src/HOL/Library/Liminf_Limsup.thy
changeset 61973 0c7e865fa7cb
parent 61969 e01015e49041
child 62049 b0f941e207cf
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 29 23:50:44 2015 +0100
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Dec 30 11:21:54 2015 +0100
     1.3 @@ -192,7 +192,7 @@
     1.4  lemma lim_imp_Liminf:
     1.5    fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
     1.6    assumes ntriv: "\<not> trivial_limit F"
     1.7 -  assumes lim: "(f ---> f0) F"
     1.8 +  assumes lim: "(f \<longlongrightarrow> f0) F"
     1.9    shows "Liminf F f = f0"
    1.10  proof (intro Liminf_eqI)
    1.11    fix P assume P: "eventually P F"
    1.12 @@ -231,7 +231,7 @@
    1.13  lemma lim_imp_Limsup:
    1.14    fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
    1.15    assumes ntriv: "\<not> trivial_limit F"
    1.16 -  assumes lim: "(f ---> f0) F"
    1.17 +  assumes lim: "(f \<longlongrightarrow> f0) F"
    1.18    shows "Limsup F f = f0"
    1.19  proof (intro Limsup_eqI)
    1.20    fix P assume P: "eventually P F"
    1.21 @@ -271,7 +271,7 @@
    1.22    fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
    1.23    assumes ntriv: "\<not> trivial_limit F"
    1.24      and lim: "Liminf F f = f0" "Limsup F f = f0"
    1.25 -  shows "(f ---> f0) F"
    1.26 +  shows "(f \<longlongrightarrow> f0) F"
    1.27  proof (rule order_tendstoI)
    1.28    fix a assume "f0 < a"
    1.29    with assms have "Limsup F f < a" by simp
    1.30 @@ -290,7 +290,7 @@
    1.31  
    1.32  lemma tendsto_iff_Liminf_eq_Limsup:
    1.33    fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
    1.34 -  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
    1.35 +  shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
    1.36    by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
    1.37  
    1.38  lemma liminf_subseq_mono: