hasDerivWithinAt_neg — Mathlib

English

The derivative of the negation map within a set s at x is −1; i.e., the local linear approximation is given by −1.

Русский

Производная от отрицания внутри множества s в точке x равна −1; локальное линейное приближение задаётся как −1.

LaTeX

$$$ \frac{d}{dt}(-t)\big|_{t=x} = -1 $$$

Lean4

theorem hasDerivWithinAt_neg : HasDerivWithinAt Neg.neg (-1) s x :=
  hasDerivAtFilter_neg _ _

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