English
If f is meromorphic on U, then around x there exists p such that f is analytic except possibly at isolated points in a neighborhood.
Русский
Если f мероморфна на U, то в окрестности x существует множество точек, где f аналитична, за исключением изолированных точек.
LaTeX
$$$\\exists$ neighborhood of x in U where f is analytic except possibly at discrete set.$$
Lean4
/-- Variant of `meromorphicTrailingCoeffAt_of_order_eq_finite`: Definition of the trailing coefficient
in case where `f` is meromorphic of finite order and a presentation is given.
-/
theorem meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE {n : ℤ} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
(h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z) : meromorphicTrailingCoeffAt f x = g x :=
by
have h₄ : MeromorphicAt f x := by
rw [MeromorphicAt.meromorphicAt_congr h]
fun_prop
have : meromorphicOrderAt f x = n :=
by
simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]
use g, h₁g, h₂g
exact h
simp_all [meromorphicTrailingCoeffAt_of_eq_nhdsNE h₁g]
