equivMultiset — Mathlib

English

The symmetric square is equivalent to the set of all multisets of cardinality two.

Русский

Симметрическая пара эквивалентна множествам (мультiset) с размерностью два.

LaTeX

$$$\\mathrm{Sym}^2(\\alpha) \\simeq \\{\, s : \\mathrm{Multiset}(\\alpha) \\mid \\mathrm{card}(s)=2 \\,\\}$$$

Lean4

/-- The symmetric square is equivalent to multisets of cardinality
two. (This is currently a synonym for `equivSym`, but it's provided
in case the definition for `Sym` changes.) -/
def equivMultiset (α : Type*) : Sym2 α ≃ { s : Multiset α // Multiset.card s = 2 } :=
  equivSym α

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