add — Mathlib

English

If f and g are differentiable within s at x, then f + g is differentiable within s at x.

Русский

Если f и g дифференцируемы внутри s в x, то f + g дифференцируема внутри s в x.

LaTeX

$$$\displaystyle \text{DifferentiableWithinAt } 𝕜 f s x \land \text{DifferentiableWithinAt } 𝕜 g s x \Rightarrow \text{DifferentiableWithinAt } 𝕜 (f+g) s x.$$$

Lean4

@[fun_prop]
theorem add (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
    DifferentiableWithinAt 𝕜 (f + g) s x :=
  (hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).differentiableWithinAt

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