fderivWithin_add_const

Mathlib.Analysis.Calculus.FDeriv.Add

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

English

Adding a constant to the input does not change the derivative within s.

Русский

При прибавлении константы к аргументу производная внутри s не меняется.

LaTeX

$$$$ fderivWithin 𝕜 (f) s x = fderivWithin 𝕜 (f) s x.$$$$

Lean4

@[simp]
theorem fderivWithin_add_const (c : F) : fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x := by
  classical simp [fderivWithin]

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

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

Разделы

Аффилиация

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