differentiableAt_neg_iff — Mathlib

English

Differentiability of f at x is equivalent to differentiability of −f at x.

Русский

Дифференцируемость f в x эквивалентна дифференцируемости −f в x.

LaTeX

$$$$ DifferentiableAt\ 𝕜\ f\ x \iff DifferentiableAt\ 𝕜\ (-f)\ x. $$$$

Lean4

@[simp]
theorem differentiableAt_neg_iff : DifferentiableAt 𝕜 (-f) x ↔ DifferentiableAt 𝕜 f x :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

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