differentiable_neg_iff — Mathlib

English

Let f: E → F be a function between normed spaces over 𝕜. Then f is differentiable everywhere iff the function −f is differentiable everywhere.

Русский

Пусть f: E → F – функция между нормированными пространствами над 𝕜. Тогда f дифференцируемая повсеместно тогда и только тогда, когда −f дифференцируема повсеместно.

LaTeX

$$$\text{Differentiable}_{\mathbb{K}}(-f) \iff \text{Differentiable}_{\mathbb{K}}(f)$$$

Lean4

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

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