# Multiset coercion to type #

This module defines a CoeSort 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 a Type*. Each x : m has two components. The first, x.1, can be obtained via the coercion ↑x : α, and it yields the underlying element of the multiset. The second, x.2, is a term of Fin (m.count x), and its function is to ensure each term appears with the correct multiplicity. Note that this coercion requires DecidableEq α due to the definition using Multiset.count.
• Multiset.toEnumFinset is a Finset version of this.
• Multiset.coeEmbedding is the embedding m ↪ α × ℕ, whose first component is the coercion and whose second component enumerates elements with multiplicity.
• Multiset.coeEquiv is the equivalence m ≃ m.toEnumFinset.

## Tags #

multiset enumeration

def Multiset.ToType {α : Type u_1} [] (m : ) :
Type u_1

Auxiliary definition for the CoeSort instance. This prevents the CoeOut m α instance from inadvertently applying to other sigma types.

Equations
• m.ToType = ((x : α) × Fin ())
Instances For
instance instCoeSortMultisetType {α : Type u_1} [] :
CoeSort () (Type u_1)

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 from different values of i.

Equations
• instCoeSortMultisetType = { coe := Multiset.ToType }
@[reducible, match_pattern]
def Multiset.mkToType {α : Type u_1} [] (m : ) (x : α) (i : Fin ()) :
m.ToType

Constructor for terms of the coercion of m to a type. This helps Lean pick up the correct instances.

Equations
• m.mkToType x i = x, i
Instances For
instance instCoeSortMultisetType.instCoeOutToType {α : Type u_1} [] {m : } :
CoeOut m.ToType α

As a convenience, there is a coercion from m : Type* to α by projecting onto the first component.

Equations
• instCoeSortMultisetType.instCoeOutToType = { coe := fun (x : m.ToType) => x.fst }
theorem Multiset.coe_mk {α : Type u_1} [] {m : } {x : α} {i : Fin ()} :
(m.mkToType x i).fst = x
@[simp]
theorem Multiset.coe_mem {α : Type u_1} [] {m : } {x : m.ToType} :
x.fst m
@[simp]
theorem Multiset.forall_coe {α : Type u_1} [] {m : } (p : m.ToTypeProp) :
(∀ (x : m.ToType), p x) ∀ (x : α) (i : Fin ()), p x, i
@[simp]
theorem Multiset.exists_coe {α : Type u_1} [] {m : } (p : m.ToTypeProp) :
(∃ (x : m.ToType), p x) ∃ (x : α) (i : Fin ()), p x, i
instance instFintypeElemProdNatSetOfLtSndCountFst {α : Type u_1} [] {m : } :
Fintype {p : α × | p.2 < Multiset.count p.1 m}
Equations
• instFintypeElemProdNatSetOfLtSndCountFst = Fintype.ofFinset (m.toFinset.biUnion fun (x : α) => Finset.map { toFun := , inj' := } ())
def Multiset.toEnumFinset {α : Type u_1} [] (m : ) :

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.

Equations
Instances For
@[simp]
theorem Multiset.mem_toEnumFinset {α : Type u_1} [] (m : ) (p : α × ) :
p m.toEnumFinset p.2 < Multiset.count p.1 m
theorem Multiset.mem_of_mem_toEnumFinset {α : Type u_1} [] {m : } {p : α × } (h : p m.toEnumFinset) :
p.1 m
theorem Multiset.toEnumFinset_mono {α : Type u_1} [] {m₁ : } {m₂ : } (h : m₁ m₂) :
m₁.toEnumFinset m₂.toEnumFinset
@[simp]
theorem Multiset.toEnumFinset_subset_iff {α : Type u_1} [] {m₁ : } {m₂ : } :
m₁.toEnumFinset m₂.toEnumFinset m₁ m₂
@[simp]
theorem Multiset.coeEmbedding_apply {α : Type u_1} [] (m : ) (x : m.ToType) :
m.coeEmbedding x = (x.fst, x.snd)
def Multiset.coeEmbedding {α : Type u_1} [] (m : ) :
m.ToType α ×

The embedding from a multiset into α × ℕ where the second coordinate enumerates repeats. If you are looking for the function m → α, that would be plain (↑).

Equations
• m.coeEmbedding = { toFun := fun (x : m.ToType) => (x.fst, x.snd), inj' := }
Instances For
@[simp]
theorem Multiset.coeEquiv_symm_apply_fst {α : Type u_1} [] (m : ) (x : { x : α × // x m.toEnumFinset }) :
(m.coeEquiv.symm x).fst = (x).1
@[simp]
theorem Multiset.coeEquiv_symm_apply_snd_val {α : Type u_1} [] (m : ) (x : { x : α × // x m.toEnumFinset }) :
(m.coeEquiv.symm x).snd = (x).2
@[simp]
theorem Multiset.coeEquiv_apply_coe {α : Type u_1} [] (m : ) (x : m.ToType) :
(m.coeEquiv x) = m.coeEmbedding x
def Multiset.coeEquiv {α : Type u_1} [] (m : ) :
m.ToType { x : α × // x m.toEnumFinset }

Another way to coerce a Multiset to a type is to go through m.toEnumFinset and coerce that Finset to a type.

Equations
• m.coeEquiv = { toFun := fun (x : m.ToType) => m.coeEmbedding x, , invFun := fun (x : { x : α × // x m.toEnumFinset }) => (x).1, (x).2, , left_inv := , right_inv := }
Instances For
@[simp]
theorem Multiset.toEmbedding_coeEquiv_trans {α : Type u_1} [] (m : ) :
m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun (x : α × ) => x m.toEnumFinset) = m.coeEmbedding
@[irreducible]
instance Multiset.fintypeCoe {α : Type u_1} [] {m : } :
Fintype m.ToType
Equations
theorem Multiset.map_univ_coeEmbedding {α : Type u_1} [] (m : ) :
Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset
theorem Multiset.toEnumFinset_filter_eq {α : Type u_1} [] (m : ) (x : α) :
Finset.filter (fun (p : α × ) => x = p.1) m.toEnumFinset = Finset.map { toFun := , inj' := } ()
@[simp]
theorem Multiset.map_toEnumFinset_fst {α : Type u_1} [] (m : ) :
Multiset.map Prod.fst m.toEnumFinset.val = m
@[simp]
theorem Multiset.image_toEnumFinset_fst {α : Type u_1} [] (m : ) :
Finset.image Prod.fst m.toEnumFinset = m.toFinset
@[simp]
theorem Multiset.map_univ_coe {α : Type u_1} [] (m : ) :
Multiset.map (fun (x : m.ToType) => x.fst) Finset.univ.val = m
@[simp]
theorem Multiset.map_univ {α : Type u_1} [] {β : Type u_2} (m : ) (f : αβ) :
Multiset.map (fun (x : m.ToType) => f x.fst) Finset.univ.val =
@[simp]
theorem Multiset.card_toEnumFinset {α : Type u_1} [] (m : ) :
m.toEnumFinset.card = Multiset.card m
@[simp]
theorem Multiset.card_coe {α : Type u_1} [] (m : ) :
Fintype.card m.ToType = Multiset.card m
theorem Multiset.sum_eq_sum_coe {α : Type u_1} [] [] (m : ) :
m.sum = x : m.ToType, x.fst
theorem Multiset.prod_eq_prod_coe {α : Type u_1} [] [] (m : ) :
m.prod = x : m.ToType, x.fst
theorem Multiset.sum_eq_sum_toEnumFinset {α : Type u_1} [] [] (m : ) :
m.sum = xm.toEnumFinset, x.1
theorem Multiset.prod_eq_prod_toEnumFinset {α : Type u_1} [] [] (m : ) :
m.prod = xm.toEnumFinset, x.1
theorem Multiset.sum_toEnumFinset {α : Type u_1} [] {β : Type u_2} [] (m : ) (f : αβ) :
xm.toEnumFinset, f x.1 x.2 = x : m.ToType, f x.fst x.snd
theorem Multiset.prod_toEnumFinset {α : Type u_1} [] {β : Type u_2} [] (m : ) (f : αβ) :
xm.toEnumFinset, f x.1 x.2 = x : m.ToType, f x.fst x.snd