analyticOrderAt_eq_top — Mathlib

English

The order at z0 is top (∞) iff f vanishes in a neighborhood of z0.

Русский

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

LaTeX

$$$\text{analyticOrderAt f z_0} = \top \;\;\Longleftrightarrow\;\; \forall^\nhds z \; (f z = 0)$$$

Lean4

/-- The order of a function `f` at a `z₀` is infinity iff `f` vanishes locally around `z₀`. -/
theorem analyticOrderAt_eq_top : analyticOrderAt f z₀ = ⊤ ↔ ∀ᶠ z in 𝓝 z₀, f z = 0
    where
  mp hf := by unfold analyticOrderAt at hf; split_ifs at hf with h <;> simp [*] at *
  mpr hf := by unfold analyticOrderAt; simp [hf, analyticAt_congr hf, analyticAt_const]

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