English
Let E be a real normed space and f,g : E → R be differentiable with f(x) ≠ 0 for all x. Then the function x ↦ f(x)^{g(x)} is differentiable on E.
Русский
Пусть E — нормированное пространство над R и f,g : E → R дифференцируемы, причём f(x) ≠ 0 для всех x. Тогда функция x ↦ f(x)^{g(x)} дифференцируема на E.
LaTeX
$$$ (\forall E [\text{NormedAddCommGroup } E] [\text{NormedSpace } \mathbb{R} E])\, (f,g : E \to \mathbb{R}) \, (\text{Differentiable } \mathbb{R} f) \, (\text{Differentiable } \mathbb{R} g) \, (\forall x, f(x) \neq 0) \Rightarrow \text{Differentiable } \mathbb{R} (x \mapsto f(x)^{g(x)}) $$$
Lean4
@[fun_prop]
theorem rpow (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) (h : ∀ x, f x ≠ 0) :
Differentiable ℝ fun x => f x ^ g x := fun x => (hf x).rpow (hg x) (h x)
