hasStrictDerivAt_rpow_const — Mathlib

English

For p ∈ ℝ and nonzero x, the map x ↦ x^p is ContDiffAt at x.

Русский

Для p ∈ ℝ и ненулевого x функция x^p является ContDiffAt в точке x.

LaTeX

$$$\\forall p\\in\\mathbb{R},\\forall x\\neq 0:\\ ContDiffAt\\mathbb{R}\\;n\\ (x\\mapsto x^p)\\ x.$$$

Lean4

theorem hasStrictDerivAt_rpow_const {x p : ℝ} (hx : x ≠ 0 ∨ 1 ≤ p) :
    HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x :=
  ContDiffAt.hasStrictDerivAt' (contDiffAt_rpow_const (by rwa [← Nat.cast_one] at hx)) (hasDerivAt_rpow_const hx) le_rfl

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