eq_zero_of_norm_pow_within — Mathlib

English

If a function f is bounded by a multiple of the n-th power of distance to x0 within a set s and x0 ∈ s with n ≠ 0, then f(x0) = 0.

Русский

Если функция ограничена мультипликатором расстояния до x0 в рамках множества s и x0 ∈ s при n ≠ 0, то f(x0) = 0.

LaTeX

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

Lean4

theorem eq_zero_of_norm_pow_within {f : E'' → F''} {s : Set E''} {x₀ : E''} {n : ℕ}
    (h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : n ≠ 0) : f x₀ = 0 :=
  mem_of_mem_nhdsWithin hx₀ h.eq_zero_imp <| by simp_rw [sub_self, norm_zero, zero_pow hn]

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