pow — Mathlib

English

In an algebraic setting, for any differentiable f, the map x ↦ x^n is differentiable on any set.

Русский

В алгебраическом контексте для любой дифференцируемой функции f отображение x ↦ x^n дифференцируемо на любом множестве.

LaTeX

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

Lean4

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

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