English
If each f_i is ContDiffAt 𝕜 n at x, then the sum is ContDiffAt 𝕜 n at x.
Русский
Если каждый f_i имеет ContDiffAt 𝕜 n в точке x, то сумма имеет ContDiffAt 𝕜 n в точке x.
LaTeX
$$∀ i, ContDiffAt 𝕜 n (f_i) x → ContDiffAt 𝕜 n (\sum i) x$$
Lean4
@[fun_prop]
theorem sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {x : E} (h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) :
ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x := by rw [← contDiffWithinAt_univ] at *; exact ContDiffWithinAt.sum h