add — Mathlib

English

If f and g are differentiable within at s, then their sum is differentiable within at s with derivative the sum of their derivatives.

Русский

Если f и g дифференцируемы внутри at на s, то их сумма дифференцируема внутри на s с производной суммой производных.

LaTeX

$$$\text{MDifferentiableWithinAt } I I' f s x \land \text{MDifferentiableWithinAt } I I' g s x \Rightarrow \text{MDifferentiableWithinAt } I I' (f+g) s x$$$

Lean4

theorem add {s : Set M} (hf : MDifferentiableOn I 𝓘(𝕜, E') f s) (hg : MDifferentiableOn I 𝓘(𝕜, E') g s) :
    MDifferentiableOn I 𝓘(𝕜, E') (f + g) s := fun x hx ↦ (hf x hx).add (hg x hx)

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