rpow_const — Mathlib

English

If f is differentiable on a set s, and f(x) ≠ 0 for all x in s, then x ↦ f(x)^g(x) is differentiable on s whenever g is differentiable on s.

Русский

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

LaTeX

$$$ \\forall hf : \\text{DifferentiableOn } \\mathbb{R} f s, \\; \\forall hg : \\text{DifferentiableOn } \\mathbb{R} g s, \\; (\\forall x \\in s, f(x) \\neq 0) \\Rightarrow \\text{DifferentiableOn } \\mathbb{R} (x \\mapsto f(x)^{g(x)}) s$$

Lean4

@[fun_prop]
theorem rpow_const (hf : DifferentiableOn ℝ f s) (h : ∀ x ∈ s, f x ≠ 0 ∨ 1 ≤ p) :
    DifferentiableOn ℝ (fun x => f x ^ p) s := fun x hx => (hf x hx).rpow_const (h x hx)

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