Behaviour as the Imaginary Part Tends to Infinity

Auxiliary lemmas about the atImInfty filter on the upper half-plane.

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

theorem ne_zero_of_tendsto_ne_zero {f : UpperHalfPlane → ℂ} {c : ℂ} (hc : c ≠ 0) (hf : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds c)) : f ≠ 0

If f tends to c ≠ 0 at infinity, then f ≠ 0 as a function.

This packages the common argument: if f = 0, then f → 0, but also f → c by hypothesis. By uniqueness of limits, 0 = c, contradicting c ≠ 0.