deriv_comp_sub_const

Mathlib.Analysis.Calculus.Deriv.Shift

URI: https://scilib.ai/kg/mathlib#deriv_comp_sub_const

English

Derivative of x ↦ f(x − a) equals deriv f at x − a.

Русский

Производная функции x ↦ f(x − a) равна производной f в x − a.

LaTeX

$$$\\mathrm{deriv}(f(x - a))\\; x = \\mathrm{deriv}(f)(x - a)$$$

Lean4

theorem deriv_comp_sub_const : deriv (fun x ↦ f (x - a)) x = deriv f (x - a) := by
  simp_rw [sub_eq_add_neg, deriv_comp_add_const]

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

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

Разделы

Аффилиация

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