English
If h_i asserts DifferentiableWithinAt 𝕜 (A_i) s x for all i in u, then the sum ∑ i∈u A_i has DifferentiableWithinAt 𝕜 with respect to s at x equal to the sum of the individual differentiabilities.
Русский
Если для каждого i в u имеется DifferentiableWithinAt 𝕜 (A_i) s x, то сумма обладает DifferentiableWithinAt 𝕜 на s в x, равной сумме индивидуальных свойств.
LaTeX
$$$\operatorname{DifferentiableWithinAt}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\ s\ x$$
Lean4
@[fun_prop]
theorem sum (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) : DifferentiableWithinAt 𝕜 (∑ i ∈ u, A i) s x :=
HasFDerivWithinAt.differentiableWithinAt <| HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt
