fun_pow — Mathlib

English

If f is differentiable within a set s, then f^n is differentiable within s for every natural n.

Русский

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

LaTeX

$$$\\text{DifferentiableWithinAt}_{\\mathbb{K}}(f\\,s)\\Rightarrow \\forall n\\in\\mathbb{N}, \\text{DifferentiableWithinAt}_{\\mathbb{K}}(f^n\\,s)$$$

Lean4

@[simp, fun_prop]
theorem fun_pow (hf : DifferentiableAt 𝕜 f x) (n : ℕ) : DifferentiableAt 𝕜 (fun x => f x ^ n) x :=
  differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n

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