const_cpow — Mathlib

English

If f is differentiable at x and g is differentiable at x, then f(x)^g(x) is differentiable at x provided f(x) lies in slitPlane.

Русский

Если f и g дифференцируемы в точке x и f(x) лежит в slitPlane, то f(x)^g(x) дифференцируемо в x.

LaTeX

$$$\\\\forall E, f,g, x, s, \\text{ DifferentiableAt } f x, \\; \\text{DifferentiableAt } g x \\\\Rightarrow \\text{DifferentiableAt } (x \\mapsto f(x)^{g(x)}) x$$$

Lean4

@[fun_prop]
theorem const_cpow (hf : DifferentiableAt ℂ f x) (h0 : c ≠ 0 ∨ f x ≠ 0) : DifferentiableAt ℂ (fun x => c ^ f x) x :=
  (hf.hasFDerivAt.const_cpow h0).differentiableAt

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