eq_nhdsNE_toMeromorphicNFAt — Mathlib

English

If f is meromorphic at x, then f coincides with its normal form on the punctured neighborhood of x.

Русский

Если f мероморфна в x, то она совпадает с своей нормальной формой на удалённой точке окрестности x.

LaTeX

$$$MeromorphicAt\ f\ x \Rightarrow f =^{nhdsWithin\ x\ (\complement\{x\})} toMeromorphicNFAt\ f\ x$$$

Lean4

/-- Conversion to normal form at `x` changes the value only at x. -/
theorem eq_nhdsNE_toMeromorphicNFAt (hf : MeromorphicAt f x) : f =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x :=
  eventually_nhdsWithin_of_forall (fun _ hz ↦ hf.eqOn_compl_singleton_toMeromorphicNFAt hz)

Похожие утверждения