const_cpow — Mathlib

English

If f is differentiable within s and c ≠ 0 or f(x) ≠ 0, then x ↦ c^{f(x)} is differentiable within s with the cpow formula.

Русский

Если f дифференцируема внутри s и c ≠ 0 или f(x) ≠ 0, то x ↦ c^{f(x)} дифференцируемо внутри s по формуле cpow.

LaTeX

$$$\\\\forall f, s, x, c, DifferentiableWithinAt \\mathbb{C} f s x \\\\Rightarrow \\\\text{DifferentiableWithinAt } (x \\mapsto c^{f(x)}) s x$$$

Lean4

@[fun_prop]
theorem const_cpow (hf : DifferentiableWithinAt ℂ f s x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
    DifferentiableWithinAt ℂ (fun x => c ^ f x) s x :=
  (hf.hasFDerivWithinAt.const_cpow h0).differentiableWithinAt

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