meromorphicAt — Mathlib

English

If f is analytic at x, then it is meromorphic at x.

Русский

Если функция аналитична в точке x, то она мероморфна в точке x.

LaTeX

$$$\text{MeromorphicAt } f x \text{ holds whenever } \text{AnalyticAt } f x.$$$

Lean4

@[fun_prop]
theorem meromorphicAt {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : MeromorphicAt f x :=
  ⟨0, by simpa only [pow_zero, one_smul]⟩
    /- Analogue of the principle of isolated zeros for an analytic function: if a function is
    meromorphic at `z₀`, then either it is identically zero in a punctured neighborhood of `z₀`, or it
    does not vanish there at all. -/

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