changeset 62975 | 1d066f6ab25d |
parent 62648 | ee48e0b4f669 |
child 63040 | eb4ddd18d635 |
--- a/src/HOL/Library/Extended_Real.thy Thu Apr 14 12:17:44 2016 +0200 +++ b/src/HOL/Library/Extended_Real.thy Thu Apr 14 15:48:11 2016 +0200 @@ -3547,7 +3547,7 @@ using Liminf_le_Limsup[OF assms, of f] by auto -lemma convergent_ereal: +lemma convergent_ereal: -- \<open>RENAME\<close> fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}" shows "convergent X \<longleftrightarrow> limsup X = liminf X" using tendsto_iff_Liminf_eq_Limsup[of sequentially]