English
If UniqueDiffWithinAt 𝕜 s x and h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A_i) s x, then fderivWithin 𝕜 (∑ i∈u A_i) s x = ∑ i∈u fderivWithin 𝕜 (A_i) s x.
Русский
Если UniqueDiffWithinAt 𝕜 s x и все A_i дифференцируемы внутри s в x, тогда производная внутри суммы равна сумме производных внутри s.
LaTeX
$$$\operatorname{fderivWithin}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\ s\ x = \sum_{i\in u} \operatorname{fderivWithin}_{\mathbb{k}}\left(A_i\right)\ s\ x$$$
Lean4
theorem fderivWithin_fun_sum (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
fderivWithin 𝕜 (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x :=
(HasFDerivWithinAt.fun_sum fun i hi => (h i hi).hasFDerivWithinAt).fderivWithin hxs
