English
Let f be meromorphic at x. Then f vanishes eventually in a punctured neighborhood of x if and only if f vanishes frequently in punctured neighborhoods.
Русский
Пусть f есть мероморфна в точке x. Тогда нули f образуют как можно более частые точки в проколотом окрестном окружении x тогда и только тогда, когда функция равна нулю на проколотом окружении в окрестности x почти всюду.
LaTeX
$$$\\text{If } f \\text{ is meromorphic at } x, \\\\ (\\exists^\\ast z \\text{ in } \\mathcal{N}_{x}^{\\neq} : f(z)=0) \\,\\iff\\, f\\big|_{\\mathcal{N}_{x}^{\\neq}} \\equiv 0$$$
Lean4
/-- The principle of isolated zeros: If `f` is meromorphic at `x`, then `f` vanishes eventually in a
punctured neighborhood of `x` iff it vanishes frequently in punctured neighborhoods.
See `AnalyticAt.frequently_zero_iff_eventually_zero` for a stronger result in the analytic case.
-/
theorem frequently_zero_iff_eventuallyEq_zero (hf : MeromorphicAt f x) : (∃ᶠ z in 𝓝[≠] x, f z = 0) ↔ f =ᶠ[𝓝[≠] x] 0 :=
⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right, fun h ↦ h.frequently⟩
