congr_deriv — Mathlib

English

If h : HasDerivWithinAt f f' s x and h' : f' = g', then HasDerivWithinAt f g' s x.

Русский

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

LaTeX

$$$HasDerivWithinAt f f' s x \\rightarrow (f' = g') \\rightarrow HasDerivWithinAt f g' s x$$$

Lean4

theorem congr_deriv (h : HasDerivWithinAt f f' s x) (h' : f' = g') : HasDerivWithinAt f g' s x :=
  HasFDerivWithinAt.congr_fderiv h <| congr_arg _ h'

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