src/HOL/Library/Extended_Real.thy
changeset 57025 e7fd64f82876
parent 56993 e5366291d6aa
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -2168,6 +2168,10 @@
     1.4      by (auto simp: order_tendsto_iff)
     1.5  qed
     1.6  
     1.7 +lemma tendsto_PInfty_eq_at_top:
     1.8 +  "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
     1.9 +  unfolding tendsto_PInfty filterlim_at_top_dense by simp
    1.10 +
    1.11  lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
    1.12    unfolding tendsto_def
    1.13  proof safe