fun_neg — Mathlib

English

For all f, the negation of a function preserves the derivative within a set s at x.

Русский

Отрицание функции сохраняет производную внутри множества s в точке x.

LaTeX

$$$\\text{derivWithin}(\\lambda y. -f(y), s, x) = -\\text{derivWithin}(f, s, x).$$$

Lean4

theorem fun_neg : derivWithin (fun y ↦ -f y) s x = -derivWithin f s x :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · simp only [derivWithin, fderivWithin_fun_neg hsx, ContinuousLinearMap.neg_apply]
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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