mem_sum — Mathlib

English

A consequence of the multiset sum membership: b ∈ ∑ x ∈ s, f x iff ∃ a ∈ s, b ∈ f a.

Русский

Следствие по членству в сумме финсет: b ∈ ∑ x ∈ s, f x эквивалентно ∃ a ∈ s: b ∈ f a.

LaTeX

$$$$ b \\in \\sum_{x \\in s} f(x) \\iff \\exists a \\in s, b \\in f(a) $$$$

Lean4

@[deprecated Multiset.mem_sum (since := "2025-08-24")]
theorem _root_.Finset.mem_sum {f : ι → Multiset M} (s : Finset ι) (b : M) : (b ∈ ∑ x ∈ s, f x) ↔ ∃ a ∈ s, b ∈ f a :=
  Multiset.mem_sum

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