congr_deriv

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#HasDerivAt.congr_deriv

English

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

Русский

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

LaTeX

$$$HasStrictDerivAt f f' x \\rightarrow (f' = g') \\rightarrow HasStrictDerivAt f g' x$$$

Lean4

theorem congr_deriv (h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x :=
  HasFDerivAt.congr_fderiv h <| congr_arg _ h'

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

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

Разделы

Аффилиация

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