fun_add — Mathlib

English

If f and g are differentiable within a set s at x, then the function y ↦ f(y) + g(y) is differentiable within s at x.

Русский

Пусть функции f и g дифференцируемы внутри множества s в точке x; тогда функция y ↦ f(y) + g(y) дифференцируема внутри 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 fun_add (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
    DifferentiableWithinAt 𝕜 (fun y => f y + g y) s x :=
  (hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).differentiableWithinAt

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