deriv_const_sub

Mathlib.Analysis.Calculus.Deriv.Add

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

English

For any c, HasDerivAt (λ x, f x − c) f' x iff HasDerivAt f f' x.

Русский

Для любого c HasDerivAt (λ x, f x − c) f' x эквивалентно HasDerivAt f f' x.

LaTeX

$$$$ HasDerivAt (\lambda x, f x - c) f' x \iff HasDerivAt f f' x. $$$$

Lean4

theorem deriv_const_sub (c : F) : deriv (fun y ↦ c - f y) x = -deriv f x := by
  simp only [← derivWithin_univ, derivWithin_const_sub]

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

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

Разделы

Аффилиация

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