English
Let E be a normed space over the complex numbers, and f,g: E → ℂ be differentiable on a subset s ⊆ E. If the image f(s) lies in the slit plane, then the map x ↦ f(x)^{g(x)} is differentiable on s.
Русский
Пусть E — нормащее дополнение над комплексными числами, и f,g: E → ℂ дифференцируемы на подмножество s ⊆ E. Если образ f(s) лежит в разрезанной плоскости, то функция x ↦ f(x)^{g(x)} дифференцируема на s.
LaTeX
$$$\\text{Let }E\\text{ be a normed space over }\\mathbb{C},\\quad f,g:E\\to\\mathbb{C},\\quad s\\subset E. \\\\ \\\\ \\text{If }f\\text{ and }g\\text{ are differentiable on }s\\text{ and }f(s)\\subseteq \\mathrm{slitPlane},\\ \\\\ x\\mapsto f(x)^{g(x)}\\text{ is differentiable on }s.$$$
Lean4
@[fun_prop]
theorem cpow (hf : DifferentiableOn ℂ f s) (hg : DifferentiableOn ℂ g s) (h0 : Set.MapsTo f s slitPlane) :
DifferentiableOn ℂ (fun x ↦ f x ^ g x) s := fun x hx ↦ (hf x hx).cpow (hg x hx) (h0 hx)
