differentiableOn_pow — Mathlib

English

For every natural n, the map x ↦ x^n is differentiable on all of E when E is a vector space over the base field; i.e., the power map is differentiable everywhere.

Русский

Для каждого натурального n отображение x^n дифференцируемо повсюду в пространстве E над основанием поля.

LaTeX

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

Lean4

theorem differentiableOn_pow (n : ℕ) {s : Set 𝔸} : DifferentiableOn 𝕜 (fun x : 𝔸 => x ^ n) s :=
  differentiableOn_id.pow n

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