hasDerivAt_add_const_iff — Mathlib

English

Adding a constant inside the argument does not change the derivative within s: derivWithin (f + c) s x = derivWithin f s x.

Русский

Добавление константы внутри аргумента не изменяет производную внутри s: derivWithin (f + c) s x = derivWithin f s x.

LaTeX

$$$derivWithin (f + c) s x = derivWithin f s x$$$

Lean4

@[simp]
theorem hasDerivAt_add_const_iff (c : F) : HasDerivAt (f · + c) f' x ↔ HasDerivAt f f' x :=
  hasDerivAtFilter_add_const_iff c

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