English
Construct a Finset that enumerates the elements of a multiset m by pairing each distinct value with an index from 0 to its multiplicity minus one.
Русский
Построим Finset, перечисляющий элементы мультимножества m, сопоставляя каждому значению уникальный индекс от 0 до кратности минус единица.
LaTeX
$$toEnumFinset (m : Multiset α) : Finset (α × ℕ) := {p : α × ℕ | p.2 < m.count p.1}.toFinset$$
Lean4
/-- Construct a finset whose elements enumerate the elements of the multiset `m`.
The `ℕ` component is used to differentiate between equal elements: if `x` appears `n` times
then `(x, 0)`, ..., and `(x, n-1)` appear in the `Finset`. -/
def toEnumFinset (m : Multiset α) : Finset (α × ℕ) :=
{p : α × ℕ | p.2 < m.count p.1}.toFinset
