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 и для всех i ∈ u A_i дифференцируемы внутри 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_sum (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) :
fderivWithin 𝕜 (∑ i ∈ u, A i) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x :=
(HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt).fderivWithin hxs
