hasDerivAtFilter_const_add_iff — Mathlib

English

The equality derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x holds under differentiability within s.

Русский

Существование равенства derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x при дифференцируемости внутри s.

LaTeX

$$$\text{DifferentiableWithinAt } f s x \land \text{DifferentiableWithinAt } g s x \Rightarrow \ derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x$$$

Lean4

theorem hasDerivAtFilter_const_add_iff (c : F) : HasDerivAtFilter (c + f ·) f' x L ↔ HasDerivAtFilter f f' x L :=
  hasFDerivAtFilter_const_add_iff c

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