neg — Mathlib

English

If f is differentiable within s at x, then −f is differentiable within s at x (alternate naming).

Русский

Если f дифференцируема внутри s в x, то −f тоже дифференцируема внутри s в x.

LaTeX

$$$$ DifferentiableWithinAt\ 𝕜\ f\ s\ x \Rightarrow DifferentiableWithinAt\ 𝕜\ (-f)\ s\ x. $$$$

Lean4

@[fun_prop]
theorem neg (h : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (-f) s x :=
  h.hasFDerivWithinAt.neg.differentiableWithinAt

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