eq_zero_of_norm_pow — Mathlib

English

If f = O_{nhds x0}(‖x−x0‖^n) and n ≠ 0, then f(x0) = 0.

Русский

Если f = O_{nhds x0}(||x−x0||^n) и n ≠ 0, то f(x0) = 0.

LaTeX

$$$\\displaystyle \\text{If } f = O_{\\mathcal{nhds}(x_0)} (\\|x-x_0\\|^n) \\text{ and } n\\neq 0, \\text{ then } f(x_0)=0.$$$

Lean4

theorem eq_zero_of_norm_pow {f : E'' → F''} {x₀ : E''} {n : ℕ} (h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n) (hn : n ≠ 0) :
    f x₀ = 0 := by
  rw [← nhdsWithin_univ] at h
  exact h.eq_zero_of_norm_pow_within (mem_univ _) hn

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