pow — Mathlib

English

If f is differentiable, then the power f^n is differentiable for every n.

Русский

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

LaTeX

$$$\\forall f:E\\to\\mathbb{A},\\ (\\mathrm{Differentiable}_{\\mathbb{K}} f)\\Rightarrow \\forall n\\in\\mathbb{N},\\ \\mathrm{Differentiable}_{\\mathbb{K}}(f^n).$$$

Lean4

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

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