# mathlibdocumentation

data.multiset.fintype

# Multiset coercion to type #

This module defines a has_coe_to_sort instance for multisets and gives it a fintype instance. It also defines multiset.to_enum_finset, 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 decidable_eq α due to multiset.count.
• multiset.to_enum_finset is a finset version of this.
• multiset.coe_embedding is the embedding m ↪ α × ℕ, whose first component is the coercion and whose second component enumerates elements with multiplicity.
• multiset.coe_equiv is the equivalence m ≃ m.to_enum_finset.

## Tags #

multiset enumeration

@[nolint]
def multiset.to_type {α : Type u_1} [decidable_eq α] (m : multiset α) :
Type u_1

Auxiliary definition for the has_coe_to_sort instance. This prevents the has_coe m α instance from inadverently applying to other sigma types. One should not use this definition directly.

Equations
@[protected, instance]
def multiset.has_coe_to_sort {α : Type u_1} [decidable_eq α] :
(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.

Equations
@[simp]
theorem multiset.coe_sort_eq {α : Type u_1} [decidable_eq α] {m : multiset α} :
@[reducible]
def multiset.mk_to_type {α : Type u_1} [decidable_eq α] (m : multiset α) (x : α) (i : fin m)) :

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

Equations
@[protected, instance]
def multiset.has_coe_to_sort.has_coe {α : Type u_1} [decidable_eq α] {m : multiset α} :
α

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

Equations
@[simp]
theorem multiset.fst_coe_eq_coe {α : Type u_1} [decidable_eq α] {m : multiset α} {x : m} :
x.fst = x
@[simp]
theorem multiset.coe_eq {α : Type u_1} [decidable_eq α] {m : multiset α} {x y : m} :
x = y x.fst = y.fst
@[simp]
theorem multiset.coe_mk {α : Type u_1} [decidable_eq α] {m : multiset α} {x : α} {i : fin m)} :
(m.mk_to_type x i) = x
@[simp]
theorem multiset.coe_mem {α : Type u_1} [decidable_eq α] {m : multiset α} {x : m} :
x m
@[protected, simp]
theorem multiset.forall_coe {α : Type u_1} [decidable_eq α] {m : multiset α} (p : m → Prop) :
(∀ (x : m), p x) ∀ (x : α) (i : fin m)), p x, i⟩
@[protected, simp]
theorem multiset.exists_coe {α : Type u_1} [decidable_eq α] {m : multiset α} (p : m → Prop) :
(∃ (x : m), p x) ∃ (x : α) (i : fin m)), p x, i⟩
@[protected, instance]
def set_of.fintype {α : Type u_1} [decidable_eq α] {m : multiset α} :
fintype {p : α × | p.snd < m}
Equations
def multiset.to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :

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
@[simp]
theorem multiset.mem_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) (p : α × ) :
p.snd <
theorem multiset.mem_of_mem_to_enum_finset {α : Type u_1} [decidable_eq α] {m : multiset α} {p : α × } (h : p m.to_enum_finset) :
p.fst m
theorem multiset.to_enum_finset_mono {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} (h : m₁ m₂) :
@[simp]
theorem multiset.to_enum_finset_subset_iff {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} :
m₁ m₂
@[simp]
theorem multiset.coe_embedding_apply {α : Type u_1} [decidable_eq α] (m : multiset α) (x : m) :
def multiset.coe_embedding {α : Type u_1} [decidable_eq α] (m : multiset α) :

The embedding from a multiset into α × ℕ where the second coordinate enumerates repeats.

If you are looking for the function m → α, that would be plain coe.

Equations
@[simp]
theorem multiset.coe_equiv_symm_apply_fst {α : Type u_1} [decidable_eq α] (m : multiset α) (x : (m.to_enum_finset)) :
@[simp]
theorem multiset.coe_equiv_apply_coe {α : Type u_1} [decidable_eq α] (m : multiset α) (x : m) :
def multiset.coe_equiv {α : Type u_1} [decidable_eq α] (m : multiset α) :

Another way to coerce a multiset to a type is to go through m.to_enum_finset and coerce that finset to a type.

Equations
@[simp]
theorem multiset.coe_equiv_symm_apply_snd_coe {α : Type u_1} [decidable_eq α] (m : multiset α) (x : (m.to_enum_finset)) :
@[protected, instance]
def multiset.fintype_coe {α : Type u_1} [decidable_eq α] {m : multiset α} :
Equations
theorem multiset.map_univ_coe_embedding {α : Type u_1} [decidable_eq α] (m : multiset α) :
theorem multiset.to_enum_finset_filter_eq {α : Type u_1} [decidable_eq α] (m : multiset α) (x : α) :
finset.filter (λ (p : α × ), x = p.fst) m.to_enum_finset = finset.map {to_fun := , inj' := _} (finset.range m))
@[simp]
theorem multiset.map_to_enum_finset_fst {α : Type u_1} [decidable_eq α] (m : multiset α) :
@[simp]
theorem multiset.image_to_enum_finset_fst {α : Type u_1} [decidable_eq α] (m : multiset α) :
@[simp]
theorem multiset.map_univ_coe {α : Type u_1} [decidable_eq α] (m : multiset α) :
@[simp]
theorem multiset.map_univ {α : Type u_1} [decidable_eq α] {β : Type u_2} (m : multiset α) (f : α → β) :
multiset.map (λ (x : m), f x) finset.univ.val = m
@[simp]
theorem multiset.card_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :
@[simp]
theorem multiset.card_coe {α : Type u_1} [decidable_eq α] (m : multiset α) :
theorem multiset.prod_eq_prod_coe {α : Type u_1} [decidable_eq α] [comm_monoid α] (m : multiset α) :
m.prod = finset.univ.prod (λ (x : m), x)
theorem multiset.sum_eq_sum_coe {α : Type u_1} [decidable_eq α] (m : multiset α) :
m.sum = finset.univ.sum (λ (x : m), x)
theorem multiset.sum_eq_sum_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :
m.sum = m.to_enum_finset.sum (λ (x : α × ), x.fst)
theorem multiset.prod_eq_prod_to_enum_finset {α : Type u_1} [decidable_eq α] [comm_monoid α] (m : multiset α) :
m.prod = m.to_enum_finset.prod (λ (x : α × ), x.fst)
theorem multiset.prod_to_enum_finset {α : Type u_1} [decidable_eq α] {β : Type u_2} [comm_monoid β] (m : multiset α) (f : α → → β) :
m.to_enum_finset.prod (λ (x : α × ), f x.fst x.snd) = finset.univ.prod (λ (x : m), f x (x.snd))
theorem multiset.sum_to_enum_finset {α : Type u_1} [decidable_eq α] {β : Type u_2} (m : multiset α) (f : α → → β) :
m.to_enum_finset.sum (λ (x : α × ), f x.fst x.snd) = finset.univ.sum (λ (x : m), f x (x.snd))