rpow — Mathlib

English

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

Русский

Пусть f и g дифференциированы в x и f(x) ≠ 0; тогда f(x)^g(x) дифференцируема в x.

LaTeX

$$$\\forall x,\\;\\text{DifferentiableAt } f x \\land \\text{DifferentiableAt } g x \\land f(x)\\neq 0\\Rightarrow \\text{DifferentiableAt } (\\lambda t. f(t)^{g(t)}) x.$$$

Lean4

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

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