multiset_sum_mem — Mathlib

English

If every element of a multiset m lies in a Subsemiring s of a nonassoc semiring, then the sum of all elements of m lies in s.

Русский

Если каждый элемент мультинеса m принадлежит Subsemiring s ⊆ R, то сумма элементов m принадлежит s.

LaTeX

$${m : Multiset R} → (∀ a ∈ m, a ∈ s) → m.sum ∈ s$$

Lean4

/-- Sum of a multiset of elements in a `Subsemiring` of a `NonAssocSemiring` is
in the `Subsemiring`. -/
protected theorem multiset_sum_mem (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
  multiset_sum_mem m

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