English
If each A_i is differentiable within s at x, then the sum ∑ i∈u A_i is differentiable within s at x with derivative the sum ∑ i∈u f_i(x).
Русский
Если каждая функция A_i дифференцируема внутри s в x, то сумма ∑ i∈u A_i дифференцируема внутри s в x, а её производная равна сумме производных.
LaTeX
$$$\operatorname{DifferentiableWithinAt}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\ s\ x \iff \sum_{i\in u} \operatorname{DifferentiableWithinAt}_{\mathbb{k}}\left(A_i\right)\ s\ x$$
Lean4
@[fun_prop]
theorem fun_sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
DifferentiableWithinAt 𝕜 (fun y => ∑ i ∈ u, A i y) s x :=
HasFDerivWithinAt.differentiableWithinAt <| HasFDerivWithinAt.fun_sum fun i hi => (h i hi).hasFDerivWithinAt
