isLittleO_pow_id — Mathlib

English

If n > 1, then the map x ↦ ‖x‖^n is little-o of the identity x ↦ x near 0.

Русский

Если n > 1, то отображение x ↦ ||x||^n есть маленькое-o по отношению к x около 0.

LaTeX

$$$\\displaystyle \\text{If } 1 < n,\\; \\|x\\|^n = o_{\\mathcal{N}_0}(\\|x\\|).$$$

Lean4

theorem isLittleO_pow_id {n : ℕ} (h : 1 < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x :=
  by
  convert isLittleO_pow_pow h (𝕜 := 𝕜)
  simp only [pow_one]

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