pow — Mathlib

English

If f is ContDiff 𝕜 n, then for every m ∈ ℕ, the map y ↦ f(y)^m is ContDiff 𝕜 n.

Русский

Если f плавна до порядка n, то для любого m ∈ ℕ функция y ↦ f(y)^m гладкая до порядка n.

LaTeX

$$$\\\\forall m \\\\in \\\\mathbb{N}, \\\\ ContDiff 𝕜 n \\\\left( f \\mapsto f^m \\right)$$

Lean4

@[fun_prop]
theorem pow {f : E → 𝔸} (hf : ContDiff 𝕜 n f) : ∀ m : ℕ, ContDiff 𝕜 n fun x => f x ^ m
  | 0 => by simpa using contDiff_const
  | m + 1 => by simpa [pow_succ] using (hf.pow m).mul hf

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