rpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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