pow — Mathlib

English

If f is differentiable at x, then f^n is differentiable at x for every natural n.

Русский

Если f дифференцируема в точке x, то f^n дифференцируема в точке x для любого натурального n.

LaTeX

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

Lean4

@[simp, fun_prop]
theorem pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) : DifferentiableAt 𝕜 (f ^ n) x :=
  hf.fun_pow n

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