src/HOL/Library/Liminf_Limsup.thy
changeset 62975 1d066f6ab25d
parent 62624 59ceeb6f3079
child 63895 9afa979137da
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Apr 14 12:17:44 2016 +0200
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Apr 14 15:48:11 2016 +0200
     1.3 @@ -555,4 +555,14 @@
     1.4      using \<open>subseq r\<close> by auto
     1.5  qed
     1.6  
     1.7 +lemma tendsto_Limsup:
     1.8 +  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
     1.9 +  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"
    1.10 +  by (subst tendsto_iff_Liminf_eq_Limsup) auto
    1.11 +
    1.12 +lemma tendsto_Liminf:
    1.13 +  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
    1.14 +  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Liminf F f) F"
    1.15 +  by (subst tendsto_iff_Liminf_eq_Limsup) auto
    1.16 +
    1.17  end