rpow — Mathlib

English

The derivative of x^p (1D) is p x^{p-1} when the condition holds.

Русский

Производная x^p (одномерная) равна p x^{p-1} при условии.

LaTeX

$$$\\text{deriv }(x^p)=p x^{p-1}\\quad\\text{ under conditions.}$$$

Lean4

@[fun_prop]
theorem rpow (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) (h : f x ≠ 0) :
    DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x := by
  -- `by exact` to deal with tricky unification.
  exact (differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prodMk hg)

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