fun_pow — Mathlib

English

Let f be a differentiable map. Then for every natural number n, the map x ↦ f(x)^n is differentiable.

Русский

Пусть f — дифференцируемая отображение. Тогда для каждого натурального n функция x ↦ f(x)^n дифференцируема.

LaTeX

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

Lean4

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

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