fun_neg — Mathlib

English

If f is differentiable within s at x, then −f is differentiable within s at x.

Русский

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

LaTeX

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

Lean4

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

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