English
MeromorphicAt f x iff there exist an integer n and analytic g at x with f(z) = (z − x)^n g(z) eventually near x.
Русский
Мероморфность f в x эквивалентна существованию n и аналитной g в x так, что почти вблизи x выполняется f(z) = (z − x)^n g(z).
LaTeX
$$$MeromorphicAt f x \iff \exists n:\mathbb{Z},\exists g:𝕜\to E, AnalyticAt 𝕜 g x \land \forallᶠ z in 𝓝[≠] x,\ f z = (z - x)^n \cdot g z$$$
Lean4
/-- If `f` is meromorphic on `U`, if `g` agrees with `f` on a codiscrete subset of `U` and outside of
`U`, then `g` is also meromorphic on `U`.
-/
theorem congr_codiscreteWithin_of_eqOn_compl (hf : MeromorphicOn f U) (h₁ : f =ᶠ[codiscreteWithin U] g)
(h₂ : Set.EqOn f g Uᶜ) : MeromorphicOn g U := by
intro x hx
apply (hf x hx).congr
simp_rw [EventuallyEq, Filter.Eventually, mem_codiscreteWithin, disjoint_principal_right] at h₁
filter_upwards [h₁ x hx] with a ha
simp at ha
tauto
