sum_apply — Mathlib

English

For any finite set s and f: ι →ᵇ β, the value at a is the sum of the values: (∑ i∈s f_i)(a) = ∑ i∈s f_i(a).

Русский

Для конечного множества s и функций f_i: a →ᵇ β вернем: (∑ i∈s f_i)(a) = ∑ i∈s f_i(a).

LaTeX

$$$\left(\sum_{i\in s} f_i\right)(a) = \sum_{i\in s} f_i(a)$$$

Lean4

theorem sum_apply {ι : Type*} (s : Finset ι) (f : ι → α →ᵇ β) (a : α) : (∑ i ∈ s, f i) a = ∑ i ∈ s, f i a := by simp

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