fst_sum — Mathlib

English

For a finite subset s and a family f of elements in the symmetrized product, the first component distributes over finite sums: fst( sum_i f(i) ) = sum_i fst(f(i)).

Русский

Для конечного множества s и семейства элементов f(i) в симметризованном произведении выполняется: fst(∑ f(i)) = ∑ fst(f(i)).

LaTeX

$$fst(∑_{i∈s} f(i)) = ∑_{i∈s} fst(f(i))$$

Lean4

theorem fst_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
    (∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst :=
  Prod.fst_sum

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