meromorphicOrderAt_of_not_meromorphicAt

English

The order of f at x is infinite if and only if f vanishes in a punctured neighborhood of x.

Русский

Порядок f в x бесконечен тогда и только тогда, когда f обращается в нуль в пунктированной окрестности x.

LaTeX

$$$meromorphicOrderAt\ f\ x = \top \iff \forall\ᶠ z\ in\ 𝓝[≠]\ x,\ f\ z = 0$$$

Lean4

@[simp]
theorem meromorphicOrderAt_of_not_meromorphicAt (hf : ¬MeromorphicAt f x) : meromorphicOrderAt f x = 0 :=
  dif_neg hf

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