[STATEMENT]
lemma eventually_int_real_at_top:
  assumes "eventually P (at_top :: real filter)"
  shows   "eventually (\<lambda>x. P (of_int x)) (at_top :: int filter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (real_of_int x)
[PROOF STEP]
using assms filterlim_of_int_at_top filterlim_iff filterlim_real_of_int_at_top
[PROOF STATE]
proof (prove)
using this:
eventually P at_top
filterlim ?f ?F at_top \<Longrightarrow> LIM x at_top. ?f (real_of_int x) :> ?F
filterlim ?f ?F2.0 ?F1.0 = (\<forall>P. eventually P ?F2.0 \<longrightarrow> (\<forall>\<^sub>F x in ?F1.0. P (?f x)))
filterlim real_of_int at_top at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (real_of_int x)
[PROOF STEP]
by blast