English
At a meromorphic point, near the point excluding it, the function is either eventually identically zero or eventually nonzero.
Русский
В окрестности точки мероморфности, исключая саму точку, функция либо становится ноль на протяжении некоторогоNeighbourhood, либо не равна нулю на протяжении этого окружения.
LaTeX
$$$\text{MeromorphicAt}(f,x) \Rightarrow \; (\forall\text{ eventually } z \neq x, f(z)=0) \lor (\forall\text{ eventually } z \neq x, f(z)\neq 0).$$$
Lean4
theorem eventually_eq_zero_or_eventually_ne_zero {f : 𝕜 → E} {z₀ : 𝕜} (hf : MeromorphicAt f z₀) :
(∀ᶠ z in 𝓝[≠] z₀, f z = 0) ∨ (∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0) :=
by
obtain ⟨n, h⟩ := hf
rcases h.eventually_eq_zero_or_eventually_ne_zero with h₁ | h₂
· left
filter_upwards [nhdsWithin_le_nhds h₁, self_mem_nhdsWithin] with y h₁y h₂y
rw [Set.mem_compl_iff, Set.mem_singleton_iff, ← sub_eq_zero] at h₂y
exact smul_eq_zero_iff_right (pow_ne_zero n h₂y) |>.mp h₁y
· right
filter_upwards [h₂, self_mem_nhdsWithin] with y h₁y h₂y
exact (smul_ne_zero_iff.1 h₁y).2
