English
If f,g: E → ℂ are differentiable on the entire space E and f never leaves the slit plane, then the map x ↦ f(x)^{g(x)} is differentiable on E.
Русский
Если f,g: E → ℂ дифференцируемы на всей пространства E и f(x) нигде не покидает разрезанную плоскость, то x ↦ f(x)^{g(x)} дифференцируема на E.
LaTeX
$$$\\text{Let }E\\text{ be a normed space over }\\mathbb{C},\\ f,g:E\\to\\mathbb{C}. \\\\ f\\text{ and }g\\text{ are differentiable on }E\\text{ and }f(E)\\subseteq\\mathrm{slitPlane}. \\\\ \\Longrightarrow\\ x\\mapsto f(x)^{g(x)}\\text{ is differentiable on }E.$$$
Lean4
@[fun_prop]
theorem cpow (hf : Differentiable ℂ f) (hg : Differentiable ℂ g) (h0 : ∀ x, f x ∈ slitPlane) :
Differentiable ℂ (fun x ↦ f x ^ g x) := fun x ↦ (hf x).cpow (hg x) (h0 x)
