Multiset coercion to type #
This module defines a hasCoeToSort
instance for multisets and gives it a Fintype
instance.
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
Finset
theory.
Main definitions #
- A coercion from
m : Multiset α
to aType*
. Forx : m
, then there is a coercion↑x : α
, andx.2
is a term ofFin (m.count x)
. The second component is what ensures each term appears with the correct multiplicity. Note that this coercion requiresdecidableEq α
due toMultiset.count
. Multiset.toEnumFinset
is aFinset
version of this.Multiset.coeEmbedding
is the embeddingm ↪ α × ℕ
, whose first component is the coercion and whose second component enumerates elements with multiplicity.Multiset.coeEquiv
is the equivalencem ≃ m.toEnumFinset
.
Tags #
multiset enumeration
Auxiliary definition for the hasCoeToSort
instance. This prevents the hasCoe m α
instance from inadvertently applying to other sigma types. One should not use this definition
directly.
Instances For
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 i
.
Constructor for terms of the coercion of m
to a type.
This helps Lean pick up the correct instances.
Instances For
As a convenience, there is a coercion from m : Type*
to α
by projecting onto the first
component.
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
.
Instances For
The embedding from a multiset into α × ℕ
where the second coordinate enumerates repeats.
If you are looking for the function m → α
, that would be plain (↑)
.
Instances For
Another way to coerce a Multiset
to a type is to go through m.toEnumFinset
and coerce
that Finset
to a type.