fun_pow — Mathlib

English

If f is differentiable on a set s, then the map x ↦ f(x)^n is differentiable on s for every natural n.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem fun_pow (hf : DifferentiableOn 𝕜 f s) (n : ℕ) : DifferentiableOn 𝕜 (fun x => f x ^ n) s := fun x h =>
  (hf x h).pow n

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