zpow — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{DifferentiableAt } 𝕜 f a \\Rightarrow \\text{DifferentiableAt } 𝕜 (f^m) a$$$

Lean4

theorem zpow (hf : DifferentiableOn 𝕜 f t) (h : (∀ x ∈ t, f x ≠ 0) ∨ 0 ≤ m) : DifferentiableOn 𝕜 (fun x => f x ^ m) t :=
  fun x hx => (hf x hx).zpow <| h.imp_left fun h => h x hx

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