zpow — Mathlib

English

If f is differentiable within at a and f(a) satisfies the nonzero or nonneg condition, then f^m is differentiable within at at a.

Русский

Если f дифференцируема внутри в точке a и значение f(a) удовлетворяет условию, то f(a)^m дифференцируема внутри в точке a.

LaTeX

$$$\\text{DifferentiableWithinAt } 𝕜 f t a \\Rightarrow \\text{DifferentiableWithinAt } 𝕜 (\\lambda x, f x)^m t a$$$

Lean4

theorem zpow (hf : DifferentiableAt 𝕜 f a) (h : f a ≠ 0 ∨ 0 ≤ m) : DifferentiableAt 𝕜 (fun x => f x ^ m) a :=
  (differentiableAt_zpow.2 h).comp a hf

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