rpow — Mathlib

English

If f,g are differentiable on a set s and f does not vanish on s, then x ↦ f(x)^{g(x)} is differentiable on s.

Русский

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

LaTeX

$$$\\forall s\\subseteq\\mathbb{E},\\; (\\forall x\\in s, f(x)\\neq 0) \\Rightarrow \\text{DifferentiableOn } (\\lambda x. f(x)^{g(x)})$ на s.$$

Lean4

@[fun_prop]
theorem rpow (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) (h : ∀ x ∈ s, f x ≠ 0) :
    DifferentiableOn ℝ (fun x => f x ^ g x) s := fun x hx => (hf x hx).rpow (hg x hx) (h x hx)

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