meromorphicOrderAt_nonneg — Mathlib

English

If f is analytic at x, then its meromorphic order at x is nonnegative.

Русский

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

LaTeX

$$$0 \\leq \\operatorname{meromorphicOrderAt} f x$$$

Lean4

/-- When seen as meromorphic functions, analytic functions have nonnegative order.
-/
theorem meromorphicOrderAt_nonneg (hf : AnalyticAt 𝕜 f x) : 0 ≤ meromorphicOrderAt f x := by
  simp [hf.meromorphicOrderAt_eq]

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