congr_fderiv

Mathlib.Analysis.Calculus.FDeriv.Congr

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

English

If f' = g' then HasFDerivWithinAt f g' x given HasFDerivWithinAt f f' x.

Русский

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

LaTeX

$$$HasFDerivWithinAt f f' s x \\Rightarrow f' = g' \\Rightarrow HasFDerivWithinAt f g' s x.$$$

Lean4

theorem congr_fderiv (h : HasFDerivAt f f' x) (h' : f' = g') : HasFDerivAt f g' x :=
  h' ▸ h

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

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

Разделы

Аффилиация

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