cpow — Mathlib

English

If f and g are differentiable within s, and f(x) lies in slitPlane, then x ↦ f(x)^{g(x)} is differentiable within s.

Русский

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

LaTeX

$$$\\\\forall f,g, DifferentiableWithinAt \\mathbb{C} f s x, DifferentiableWithinAt \\mathbb{C} g s x \\\\Rightarrow DifferentiableWithinAt \\mathbb{C} (\\\\lambda x, f(x)^{g(x)}) s x$$$

Lean4

@[fun_prop]
theorem cpow (hf : DifferentiableWithinAt ℂ f s x) (hg : DifferentiableWithinAt ℂ g s x) (h0 : f x ∈ slitPlane) :
    DifferentiableWithinAt ℂ (fun x => f x ^ g x) s x :=
  (hf.hasFDerivWithinAt.cpow hg.hasFDerivWithinAt h0).differentiableWithinAt

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