English
If meromorphicOrderAt f x < 0, then f tends to infinity along the punctured neighborhood of x in the cobounded sense.
Русский
Если meromorphicOrderAt f x < 0, то f стремится к бесконечности по пунктированной окрестности x в смысле cobounded.
LaTeX
$$$\text{If } meromorphicOrderAt f x < 0,\ Tendsto\ f\ (\mathcal{N}_{\neq} x)\ \text{toCobounded}$$$
Lean4
/-- The order of a meromorphic function `f` at `z₀` is finite iff `f` does not have
any zeros in a sufficiently small neighborhood of `z₀`.
-/
theorem meromorphicOrderAt_ne_top_iff_eventually_ne_zero {f : 𝕜 → E} (hf : MeromorphicAt f x) :
meromorphicOrderAt f x ≠ ⊤ ↔ ∀ᶠ x in 𝓝[≠] x, f x ≠ 0 :=
by
constructor
· intro h
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
filter_upwards [h₃g, self_mem_nhdsWithin,
eventually_nhdsWithin_of_eventually_nhds ((h₁g.continuousAt.ne_iff_eventually_ne continuousAt_const).mp h₂g)]
simp_all [zpow_ne_zero, sub_ne_zero]
· simp_all [meromorphicOrderAt_eq_top_iff, Eventually.frequently]
