rpow_const — Mathlib

English

If f is differentiable within a set s and at x, and f(x) ≠ 0, then x ↦ f(x)^p is differentiable within s at x.

Русский

Если f дифференцируема на границе s в точке x и f(x) ≠ 0, тогда x ↦ f(x)^p дифференцируема внутри s в x.

LaTeX

$$$ \forall hf : \text{DifferentiableWithinAt } \mathbb{R} f s x, \; (f(x) \neq 0 \lor 1 \le p) \Rightarrow \text{DifferentiableWithinAt } \mathbb{R} (x \mapsto f(x)^p) s x $$$

Lean4

@[fun_prop]
theorem rpow_const (hf : DifferentiableWithinAt ℝ f s x) (h : f x ≠ 0 ∨ 1 ≤ p) :
    DifferentiableWithinAt ℝ (fun x => f x ^ p) s x :=
  (hf.hasFDerivWithinAt.rpow_const h).differentiableWithinAt

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