rpow_const_of_ne — Mathlib

English

If f is contDiffOn on s and f(x) ≠ 0 for all x ∈ s, then x ↦ f(x)^p is contDiffOn on s.

Русский

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

LaTeX

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

Lean4

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

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