sum_apply — Mathlib

English

For any finite set s and family f i ∈ C_c(α,β), the evaluation distributes over finite sums: (∑ i∈s f_i) a = ∑ i∈s f_i a for all a ∈ α.

Русский

Для любого конечного множества s и семейства f_i ∈ C_c(α,β) оценивание распределяется по сумме: (∑ i∈s f_i) a = ∑ i∈s f_i a для всех a ∈ α.

LaTeX

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

Lean4

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

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