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