toFinset_add — Mathlib

English

For multisets s and t, the Finset of their sum equals the union of the Finsets of s and t.

Русский

Для мультисетов s и t множество Finset их суммы равно объединению Finset частей s и t.

LaTeX

$$$\\operatorname{toFinset}(s + t) = \\operatorname{toFinset}(s) \\cup \\operatorname{toFinset}(t)$$$

Lean4

@[simp]
theorem toFinset_add (s t : Multiset α) : toFinset (s + t) = toFinset s ∪ toFinset t :=
  Finset.ext <| by simp

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