fun_neg — Mathlib

English

If h is HasDerivWithinAt f f' s x, then HasDerivWithinAt (fun x ↦ -f x) (-f') s x.

Русский

Если у функции внутри области s в x есть производная, то производная отрицательной функции равна отрицательной производной.

LaTeX

$$$\\forall h:\\ HasDerivWithinAt f f' s x,\\ HasDerivWithinAt (\\lambda x. -f x) (-f') s x.$$$

Lean4

nonrec theorem fun_neg (h : HasDerivWithinAt f f' s x) : HasDerivWithinAt (fun x ↦ -f x) (-f') s x :=
  h.neg

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