card_toMultiset — Mathlib

English

Mapping an unordered pair to an unordered list produces a multiset of size 2.

Русский

Отображение неупорядоченной пары в неупорядоченный список даёт мультимножество размером 2.

LaTeX

$$$$ \mathrm{toMultiset}(z) .card = 2. $$$$

Lean4

/-- Mapping an unordered pair to an unordered list produces a multiset of size `2`. -/
theorem card_toMultiset {α : Type*} (z : Sym2 α) : z.toMultiset.card = 2 :=
  by
  induction z
  simp [Sym2.toMultiset]

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