sum_mem — Mathlib

English

For a finite index set Finset and function f, if all f(i) lie in s, then the finite sum is in s.

Русский

Для конечного множества индексирования Finset и отображения f: если ∀ i ∈ t, f(i) ∈ s, то сумма по i∈t принадлежит s.

LaTeX

$$$ \bigl( \forall i \in t, f(i) \in s \bigr) \rightarrow \sum_{i \in t} f(i) \in s $$$

Lean4

/-- Sum of elements in a `Subfield` indexed by a `Finset` is in the `Subfield`. -/
protected theorem sum_mem {ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s :=
  sum_mem h

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