congr_deriv — Mathlib

English

If a function f has a strict derivative f' at x and f' = g', then f has strict derivative g' at 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 : HasStrictDerivAt f f' x) (h' : f' = g') : HasStrictDerivAt f g' x :=
  h.congr_fderiv <| congr_arg _ h'

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