analyticOrderAt_ne_zero — Mathlib

English

The analytic order is nonzero exactly when the function vanishes to positive order at z0 and is analytic there.

Русский

Порядок аналитичности не равен нулю тогда и только тогда, когда функция имеет ненулевой порядок обращения в z0 и аналитична в точке.

LaTeX

$$$\text{analyticOrderAt f z_0} \neq 0 \;\iff\; \text{AnalyticAt 𝕜 f z_0} \land f z_0 = 0$$$

Lean4

theorem analyticOrderAt_ne_zero : analyticOrderAt f z₀ ≠ 0 ↔ AnalyticAt 𝕜 f z₀ ∧ f z₀ = 0 := by
  simp [analyticOrderAt_eq_zero]

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