derivWithin_add — Mathlib

English

Let f,g be differentiable within s at x. Then derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x.

Русский

Пусть f и g дифференцируемы внутри s в x. Тогда derivWithin(f+g) s x = derivWithin f s x + derivWithin g s x.

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 derivWithin_add (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
    derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x :=
  derivWithin_fun_add hf hg

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