zpow — Mathlib

English

For any differentiable function f, if f(x) ≠ 0 or m ≤ 0 holds at all relevant x, then f^m is differentiable within at x.

Русский

Для любой дифференцируемой функции f, если f(x) ≠ 0 или m ≤ 0 выполняется на всех соответствующих x, тогда f^m дифференцируемо внутри в x.

LaTeX

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

Lean4

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

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