English
Let f: s → ℂ be differentiable on s and c ∈ ℂ. If either c ≠ 0 or f(x) ≠ 0 for all x ∈ s, then the function x ↦ c^{f(x)} is differentiable on s.
Русский
Пусть f: s → ℂ дифференцируема на s и фиксированное комплексное число c. Если либо c ≠ 0, либо для всех x ∈ s верно f(x) ≠ 0, тогда функция x ↦ c^{f(x)} дифференцируема на s.
LaTeX
$$$\\text{Let }f:s\\to\\mathbb{C}\\text{ be differentiable on }s\\text{ and }c\\in\\mathbb{C}.\\quad \\text{If }c\\ne 0\\ \\lor\\ \\forall x\\in s,\ \ f(x)\\ne 0,\\ \\text{then } x\\mapsto c^{f(x)}\\text{ is differentiable on }s.$$$
Lean4
@[fun_prop]
theorem const_cpow (hf : DifferentiableOn ℂ f s) (h0 : c ≠ 0 ∨ ∀ x ∈ s, f x ≠ 0) :
DifferentiableOn ℂ (fun x ↦ c ^ f x) s := fun x hx ↦ (hf x hx).const_cpow (h0.imp_right fun h ↦ h x hx)
