rpow — Mathlib

English

If f and g are differentiable (on the real line) and f(x) ≠ 0 for all x, then x ↦ f(x)^{g(x)} is differentiable on the whole domain.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem rpow (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (h : ∀ x, f x ≠ 0) : ContDiff ℝ n fun x => f x ^ g x :=
  contDiff_iff_contDiffAt.mpr fun x => hf.contDiffAt.rpow hg.contDiffAt (h x)

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