mem_sum — Mathlib

English

For any a ∈ M, s a Finset, and m : ι → Multiset M, membership of a in the sum ∑ i ∈ s, m i holds iff there exists i ∈ s with a ∈ m i.

Русский

Для любого a ∈ M, Finset s и m : ι → Multiset M, членство a в сумме ∑ i ∈ s, m i эквивалентно существованию i ∈ s такого, что a ∈ m i.

LaTeX

$$$$ a \\in \\sum_{i \\in s} m(i) \\quad\\Longleftrightarrow\\quad \\exists i \\in s, a \\in m(i) $$$$

Lean4

@[simp]
theorem mem_sum {a : M} {s : Finset ι} {m : ι → Multiset M} : a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i := by
  induction s using Finset.cons_induction with grind

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