English
If f and g agree on a punctured neighborhood of x, then g is meromorphic at x whenever f is.
Русский
Если f и g совпадают на окружности без точки x, то мероморфность g в x следует из мероморфности f в x.
LaTeX
$$$MeromorphicAt f x \\to (nhdsWithin x (Set.\\instHasCompl.compl (Set.singleton x))).EventuallyEq f g \\to MeromorphicAt g x$$$
Lean4
/-- With our definitions, `MeromorphicAt f x` depends only on the values of `f` on a punctured
neighbourhood of `x` (not on `f x`) -/
theorem congr {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hfg : f =ᶠ[𝓝[≠] x] g) : MeromorphicAt g x :=
by
rcases hf with ⟨m, hf⟩
refine ⟨m + 1, ?_⟩
have : AnalyticAt 𝕜 (fun z ↦ z - x) x := analyticAt_id.sub analyticAt_const
refine (this.fun_smul hf).congr ?_
rw [eventuallyEq_nhdsWithin_iff] at hfg
filter_upwards [hfg] with z hz
rcases eq_or_ne z x with rfl | hn
· simp
· rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]
