fun_add

Mathlib.Analysis.Calculus.FDeriv.Add

URI: https://scilib.ai/kg/mathlib#HasFDerivAt.fun_add

← MathLib Explorer

English

If HasFDerivAt holds for f and g at x, then f + g has derivative f' + g' at x.

Русский

Если HasFDerivAt верно для f и g в x, то f + g имеет производную f' + g' в x.

LaTeX

$$$ HasFDerivAt f f' x \rightarrow HasFDerivAt g g' x \rightarrow HasFDerivAt (f + g) (f' + g') x$$$

Lean4

@[fun_prop]
nonrec theorem fun_add (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun x => f x + g x) (f' + g') x :=
  hf.add hg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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