rpow_const_of_ne

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

URI: https://scilib.ai/kg/mathlib#ContDiffAt.rpow_const_of_ne

English

If f is contDiffAt x and f(x) ≠ 0, then x ↦ f(x)^p is contDiffAt x.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem rpow_const_of_ne (hf : ContDiffAt ℝ n f x) (h : f x ≠ 0) : ContDiffAt ℝ n (fun x => f x ^ p) x :=
  hf.rpow contDiffAt_const h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru