# Documentation

Mathlib.Data.Multiset.Fintype

# 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 a Type*. For x : m, then there is a coercion ↑x : α, and x.2 is 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 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 hasCoeToSort instance. This prevents the hasCoe m α instance from inadvertently applying to other sigma types. One should not use this definition directly.

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

@[match_pattern, reducible]
def Multiset.mkToType {α : Type u_1} [] (m : ) (x : α) (i : Fin ()) :

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

Instances For
instance instCoeSortMultisetType.instCoeOutToType {α : Type u_1} [] {m : } :

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

@[simp]
theorem Multiset.coe_eq {α : Type u_1} [] {m : } {x : } {y : } :
x.fst = y.fst x.fst = y.fst
theorem Multiset.coe_mk {α : Type u_1} [] {m : } {x : α} {i : Fin ()} :
().fst = x
@[simp]
theorem Multiset.coe_mem {α : Type u_1} [] {m : } {x : } :
x.fst m
@[simp]
theorem Multiset.forall_coe {α : Type u_1} [] {m : } (p : ) :
((x : ) → p x) (x : α) → (i : Fin ()) → p { fst := x, snd := i }
@[simp]
theorem Multiset.exists_coe {α : Type u_1} [] {m : } (p : ) :
(x, p x) x i, p { fst := x, snd := i }
instance instFintypeElemProdNatSetOfLtInstLTNatSndCountFst {α : Type u_1} [] {m : } :
Fintype {p | p.snd < Multiset.count p.fst m}
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.

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

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
@[simp]
theorem Multiset.coeEquiv_symm_apply_fst {α : Type u_1} [] (m : ) (x : { x // }) :
(().symm x).fst = (x).fst
@[simp]
theorem Multiset.coeEquiv_symm_apply_snd_val {α : Type u_1} [] (m : ) (x : { x // }) :
(().symm x).snd = (x).snd
@[simp]
theorem Multiset.coeEquiv_apply_coe {α : Type u_1} [] (m : ) (x : ) :
↑(↑() x) = ↑() x
def Multiset.coeEquiv {α : Type u_1} [] (m : ) :
{ x // }

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

Instances For
@[irreducible]
instance Multiset.fintypeCoe {α : Type u_1} [] {m : } :
theorem Multiset.map_univ_coeEmbedding {α : Type u_1} [] (m : ) :
Finset.map () Finset.univ =
theorem Multiset.toEnumFinset_filter_eq {α : Type u_1} [] (m : ) (x : α) :
Finset.filter (fun p => x = p.fst) () = Finset.map { toFun := , inj' := (_ : ) } ()
@[simp]
theorem Multiset.map_toEnumFinset_fst {α : Type u_1} [] (m : ) :
Multiset.map Prod.fst ().val = m
@[simp]
theorem Multiset.image_toEnumFinset_fst {α : Type u_1} [] (m : ) :
Finset.image Prod.fst () =
@[simp]
theorem Multiset.map_univ_coe {α : Type u_1} [] (m : ) :
Multiset.map (fun x => x.fst) Finset.univ.val = m
@[simp]
theorem Multiset.map_univ {α : Type u_1} [] {β : Type u_2} (m : ) (f : αβ) :
Multiset.map (fun x => f x.fst) Finset.univ.val =
@[simp]
theorem Multiset.card_toEnumFinset {α : Type u_1} [] (m : ) :
= Multiset.card m
@[simp]
theorem Multiset.card_coe {α : Type u_1} [] (m : ) :
= Multiset.card m
theorem Multiset.sum_eq_sum_coe {α : Type u_1} [] [] (m : ) :
= Finset.sum Finset.univ fun x => x.fst
theorem Multiset.prod_eq_prod_coe {α : Type u_1} [] [] (m : ) :
= Finset.prod Finset.univ fun x => x.fst
theorem Multiset.sum_eq_sum_toEnumFinset {α : Type u_1} [] [] (m : ) :
= Finset.sum () fun x => x.fst
theorem Multiset.prod_eq_prod_toEnumFinset {α : Type u_1} [] [] (m : ) :
= Finset.prod () fun x => x.fst
theorem Multiset.sum_toEnumFinset {α : Type u_1} [] {β : Type u_2} [] (m : ) (f : αβ) :
(Finset.sum () fun x => f x.fst x.snd) = Finset.sum Finset.univ fun x => f x.fst x.snd
theorem Multiset.prod_toEnumFinset {α : Type u_1} [] {β : Type u_2} [] (m : ) (f : αβ) :
(Finset.prod () fun x => f x.fst x.snd) = Finset.prod Finset.univ fun x => f x.fst x.snd