derivWithin_const_add

Mathlib.Analysis.Calculus.Deriv.Add

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

English

The derivative within s of c + f equals the derivative within s of f: derivWithin (c + f) s x = derivWithin f s x.

Русский

Производная внутри s от c + f равна производной внутри s от f.

LaTeX

$$$derivWithin (c + f) s x = derivWithin f s x$$$

Lean4

theorem derivWithin_const_add (c : F) : derivWithin (c + f ·) s x = derivWithin f s x := by
  simp only [derivWithin, fderivWithin_const_add]

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

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

Разделы

Аффилиация

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