neg — Mathlib

English

If f is differentiable on s with continuous derivative, then the negation -f is differentiable on s.

Русский

Если f дифференцируема на s с непрерывной производной, то функция -f дифференцируема на s.

LaTeX

$$$\text{If } \text{DiffContOnCl}(\mathit{f}, s) ,\; \text{then } \text{DiffContOnCl}( -\mathit{f}, s).$$$

Lean4

theorem neg (hf : DiffContOnCl 𝕜 f s) : DiffContOnCl 𝕜 (-f) s :=
  ⟨hf.1.neg, hf.2.neg⟩

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