sum_mem — Mathlib

English

If each evaluated element f(x) lies in S for x in a finite index set, then the finite sum over that index set lies in S.

Русский

Если каждая величина f(x) принадлежит S для x из конечного множества индексов, то их конечная сумма принадлежит S.

LaTeX

$$$$ \\forall ι,\\forall t:\\\\text{Finset}(ι),\\forall f: ι\\to A,\\ (\\\\forall x\\\\in t,\\ f x\\\\in S)\\\\Rightarrow\\ \\sum_{x\\\\in t} f x\\\\in S $$$$

Lean4

protected theorem sum_mem {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) : (∑ x ∈ t, f x) ∈ S :=
  sum_mem h

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