analyticOrderAt_ne_zero — Mathlib

English

If f and g coincide near z0, their analytic orders at z0 are equal.

Русский

Если функции совпадают в окрестности точки z0, то их аналитические порядки равны.

LaTeX

$$$\text{analyticOrderAt } f z_0 = \text{analyticOrderAt } g z_0$ whenever $f=g$ near z0$$

Lean4

/-- The order of an analytic function `f` at `z₀` is zero iff `f` does not vanish at `z₀`. -/
protected theorem analyticOrderAt_ne_zero (hf : AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ ≠ 0 ↔ f z₀ = 0 :=
  hf.analyticOrderAt_eq_zero.not_left

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