theorem Filter.eventually_atImInfty {p : UpperHalfPlane → Prop} : (∀ᶠ (x : UpperHalfPlane) in UpperHalfPlane.atImInfty, p x) ↔ ∃ (A : ℝ), ∀ (z : UpperHalfPlane), A ≤ z.im → p z

theorem Filter.tendsto_im_atImInfty : Tendsto (fun (x : UpperHalfPlane) => x.im) UpperHalfPlane.atImInfty atTop