fun_add — Mathlib

English

If f and g are differentiable at x, then their sum f + g is differentiable at x.

Русский

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

LaTeX

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

Lean4

@[simp, fun_prop]
theorem fun_add (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAt 𝕜 (fun y => f y + g y) x :=
  (hf.hasFDerivAt.add hg.hasFDerivAt).differentiableAt

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