congr_fderiv

Mathlib.Analysis.Calculus.FDeriv.Congr

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

English

If HasFDerivAt f f' x and f' = g', then HasFDerivAt f g' x.

Русский

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

LaTeX

$$$HasFDerivAt f f' x \\Rightarrow f' = g' \\Rightarrow HasFDerivAt f g' x.$$$

Lean4

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

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

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

Разделы

Аффилиация

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