fun_neg — Mathlib

English

If f has a strict derivative f' at x, then the negated function −f has the strict derivative −f' at x.

Русский

Если функция f имеет строгую производную f' в точке x, то у функции −f строгая производная −f' в точке x.

LaTeX

$$$$ HasStrictFDerivAt\ f\ f'\ x\;\Rightarrow\; HasStrictFDerivAt\ (-f)\ (-f')\ x. $$$$

Lean4

@[fun_prop]
theorem fun_neg (h : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (fun x => -f x) (-f') x :=
  (-1 : F →L[𝕜] F).hasStrictFDerivAt.comp x h

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