differentiableAt_pow — Mathlib

English

The differentiability of the power map is inherited: if f is differentiable at x, then f(x)^n is differentiable at x for all n.

Русский

Дифференцируемость отображения степени сохраняется: если f дифференцируема в x, то f(x)^n дифференцируема в x для всех n.

LaTeX

$$$\\mathrm{DifferentiableAt}_{\\mathbb{K}}(f,x) \\Rightarrow \\forall n, \\mathrm{DifferentiableAt}_{\\mathbb{K}}(f^n,x)$$$

Lean4

theorem differentiableAt_pow (n : ℕ) {x : 𝔸} : DifferentiableAt 𝕜 (fun x : 𝔸 => x ^ n) x :=
  differentiableAt_id.pow _

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