Multiset coercion to type #
This module defines a
hasCoeToSort instance for multisets and gives it a
It also defines
Multiset.toEnumFinset, which is another way to enumerate the elements of
a multiset. These coercions and definitions make it easier to sum over multisets using existing
Main definitions #
- A coercion from
m : Multiset αto a
x : m, then there is a coercion
↑x : α, and
x.2is a term of
Fin (m.count x). The second component is what ensures each term appears with the correct multiplicity. Note that this coercion requires
decidableEq αdue to
Finsetversion of this.
Multiset.coeEmbeddingis the embedding
m ↪ α × ℕ, whose first component is the coercion and whose second component enumerates elements with multiplicity.
Multiset.coeEquivis the equivalence
m ≃ m.toEnumFinset.
Create a type that has the same number of elements as the multiset.
Terms of this type are triples
⟨x, ⟨i, h⟩⟩ where
x : α,
i : ℕ, and
h : i < m.count x.
This way repeated elements of a multiset appear multiple times with different values of
Construct a finset whose elements enumerate the elements of the multiset
ℕ component is used to differentiate between equal elements: if
(x, 0), ..., and
(x, n-1) appear in the