derivWithin_neg — Mathlib

English

If x is uniquely differentiable within s, then the derivative within s of the negation is −1.

Русский

Если в окрестности s в точке x существует уникальная производность, то производная внутри s от отрицания равна −1.

LaTeX

$$$ \text{derivWithin}(-t) \, s \, x = -1 $$$

Lean4

theorem derivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin Neg.neg s x = -1 :=
  (hasDerivWithinAt_neg x s).derivWithin hxs

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