sum_apply' — Mathlib

English

Let s be a Finset and f a Finset-valued function with finitely many components. Then sum_apply' states that (∑ k ∈ s, f k) i equals ∑ k ∈ s, f k i.

Русский

Пусть s — конечный набор; тогда сумма по k дерев f k на координате i равна сумме по k: f k i.

LaTeX

$$$\big(\sum_{k \in s} f_k\big) i = \sum_{k \in s} f_k i.$$$

Lean4

theorem sum_apply' : (∑ k ∈ s, f k) i = ∑ k ∈ s, f k i :=
  map_sum (Finsupp.applyAddHom i) f s

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