sum — Mathlib

English

The product of a finite family of C^n functions is C^n within a domain.

Русский

Произведение конечного числа функций C^n внутри области — это C^n.

LaTeX

$$ContDiffWithinAt 𝕜 n (\prod i ∈ t, f i) s x$$

Lean4

@[fun_prop]
theorem sum {ι : Type*} {f : ι → E → F} {s : Finset ι} (h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) :
    ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x := by simp only [← contDiffOn_univ] at *; exact ContDiffOn.sum h

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