rpow — Mathlib

English

If f and g are continuously differentiable on a set s and f(x) ≠ 0 for all x ∈ s, then x ↦ f(x)^{g(x)} is continuously differentiable on s.

Русский

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

LaTeX

$$ContDiffOn Real n (fun x => f x ^ g x) s$$

Lean4

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

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