English
If f is meromorphic at x, then there exists a punctured neighborhood of x on which f is continuous at every point.
Русский
Если функция f мероморфна в точке x, то существует окружение x без самой точки x, на котором f непрерывна в каждой точке.
LaTeX
$$$MeromorphicAt f x \rightarrow \forallᶠ y \in 𝓝[≠] x,\ ContinuousAt f y$$$
Lean4
/-- If a function is meromorphic at a point, then it is continuous at nearby points. -/
theorem eventually_continuousAt {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, ContinuousAt f y :=
by
obtain ⟨n, h⟩ := h
have : ∀ᶠ y in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y := nhdsWithin_le_nhds h.eventually_continuousAt
filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at h'y
have : ContinuousAt (fun z ↦ ((z - x) ^ n)⁻¹) y := ContinuousAt.inv₀ (by fun_prop) (by simp [sub_eq_zero, h'y])
apply (this.smul hy).congr
filter_upwards [eventually_ne_nhds h'y] with z hz
simp [smul_smul, hz, sub_eq_zero]
