multiset_sum_mem — Mathlib

English

If every element of a multiset lies in S, then the sum of its elements lies in S.

Русский

Если каждый элемент мультинабора принадлежит S, то сумма элементов мультинабора принадлежит S.

LaTeX

$$$$ \\forall m:\\\\text{Multiset}(A),\\ (\\\\forall x\\\\in m,\\ x\\\\in S)\\\\Rightarrow m.sum\\\\in S $$$$

Lean4

protected theorem multiset_sum_mem {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S :=
  multiset_sum_mem m h

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