equal
deleted
inserted
replaced
2166 } |
2166 } |
2167 then show ?thesis |
2167 then show ?thesis |
2168 by (auto simp: order_tendsto_iff) |
2168 by (auto simp: order_tendsto_iff) |
2169 qed |
2169 qed |
2170 |
2170 |
|
2171 lemma tendsto_PInfty_eq_at_top: |
|
2172 "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)" |
|
2173 unfolding tendsto_PInfty filterlim_at_top_dense by simp |
|
2174 |
2171 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)" |
2175 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)" |
2172 unfolding tendsto_def |
2176 unfolding tendsto_def |
2173 proof safe |
2177 proof safe |
2174 fix S :: "ereal set" |
2178 fix S :: "ereal set" |
2175 assume "open S" "-\<infinity> \<in> S" |
2179 assume "open S" "-\<infinity> \<in> S" |