differentiableWithinAt_fun_neg_iff

English

If f has a derivative within s at x, then the derivative of −f within s is the negation of the derivative.

Русский

Если у f внутри s в x есть производная, то у −f внутри s её производная равна −derivative.

LaTeX

$$$$ HasFDerivWithinAt\ f\ f'\ s\ x \Rightarrow HasFDerivWithinAt\ (-f)\ (-f')\ s\ x. $$$$

Lean4

@[simp]
theorem differentiableWithinAt_fun_neg_iff :
    DifferentiableWithinAt 𝕜 (fun y => -f y) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  ⟨fun h => by simpa only [neg_neg] using h.fun_neg, fun h => h.neg⟩

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