toMultiset — Mathlib

English

There is a natural map from Sym α n to Multiset α that forgets the fixed size: toMultiset(s) = s.1.

Русский

Существует естественное отображение из Sym α n в Multiset α, которое забывает фиксированную длину: toMultiset(s) = s.1.

LaTeX

$$$\\mathrm{toMultiset}: \\mathrm{Sym}\\,\\alpha\\,n \\to \\mathrm{Multiset}\\,\\alpha$, \\; toMultiset(s) = s.1$$

Lean4

/-- The canonical map to `Multiset α` that forgets that `s` has length `n` -/
@[coe]
def toMultiset {α : Type*} {n : ℕ} (s : Sym α n) : Multiset α :=
  s.1

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