sum — Mathlib

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

Похожие утверждения