rpow — Mathlib

English

If f and g are differentiable at x and f(x) ≠ 0, then x ↦ f(x)^{g(x)} is differentiable at x.

Русский

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

LaTeX

$$ContDiffAt Real n (fun x => f x ^ g x) x$$

Lean4

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

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