hasDerivAtFilter_neg — Mathlib

English

The negation map has constant derivative −1 at every point with respect to any filter; in particular, the derivative is −1.

Русский

Отображение отрицания имеет постоянную производную −1 в каждой точке относительно любого фильтра; производная равна −1.

LaTeX

$$$ (-\mathrm{id})'(x) = -1 $$$

Lean4

theorem hasDerivAtFilter_neg : HasDerivAtFilter Neg.neg (-1) x L :=
  HasDerivAtFilter.neg <| hasDerivAtFilter_id _ _

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