English
If two meromorphic functions agree in a punctured neighborhood of x, then their orders at x are equal.
Русский
Если две мероморфные функции совпадают в пунктированной окрестности точки x, их порядки в x равны.
LaTeX
$$$ meromorphicOrderAt\ f_1\ x = meromorphicOrderAt\ f_2\ x $ при $f_1 =^{{\mathcal{N}_{≠} x}} f_2$$$
Lean4
/-- If the order of a meromorphic function is zero, then this function converges to a nonzero
limit at this point. See also the iff version `tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero`. -/
theorem tendsto_ne_zero_of_meromorphicOrderAt_eq_zero (hf : MeromorphicAt f x) (ho : meromorphicOrderAt f x = 0) :
∃ c ≠ 0, Tendsto f (𝓝[≠] x) (𝓝 c) :=
by
rcases (meromorphicOrderAt_eq_int_iff hf).1 ho with ⟨g, g_an, gx, hg⟩
refine ⟨g x, gx, ?_⟩
apply g_an.continuousAt.continuousWithinAt.tendsto.congr'
filter_upwards [hg] with y hy using by simp [hy]
