# mathlibdocumentation

data.finsupp.multiset

# Equivalence between multiset and ℕ-valued finitely supported functions #

This defines finsupp.to_multiset the equivalence between α →₀ ℕ and multiset α, along with multiset.to_finsupp the reverse equivalence and finsupp.order_iso_multiset the equivalence promoted to an order isomorphism.

noncomputable def finsupp.to_multiset {α : Type u_1} :

Given f : α →₀ ℕ, f.to_multiset is the multiset with multiplicities given by the values of f on the elements of α. We define this function as an add_equiv.

Equations
theorem finsupp.to_multiset_zero {α : Type u_1} :
theorem finsupp.to_multiset_add {α : Type u_1} (m n : α →₀ ) :
theorem finsupp.to_multiset_apply {α : Type u_1} (f : α →₀ ) :
= f.sum (λ (a : α) (n : ), n {a})
@[simp]
theorem finsupp.to_multiset_symm_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (x : α) :
@[simp]
theorem finsupp.to_multiset_single {α : Type u_1} (a : α) (n : ) :
= n {a}
theorem finsupp.to_multiset_sum {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ } (s : finset ι) :
finsupp.to_multiset (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), finsupp.to_multiset (f i))
theorem finsupp.to_multiset_sum_single {ι : Type u_3} (s : finset ι) (n : ) :
finsupp.to_multiset (s.sum (λ (i : ι), n)) = n s.val
theorem finsupp.card_to_multiset {α : Type u_1} (f : α →₀ ) :
= f.sum (λ (a : α), id)
theorem finsupp.to_multiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ) (g : α → β) :
@[simp]
theorem finsupp.prod_to_multiset {α : Type u_1} [comm_monoid α] (f : α →₀ ) :
= f.prod (λ (a : α) (n : ), a ^ n)
@[simp]
theorem finsupp.to_finset_to_multiset {α : Type u_1} [decidable_eq α] (f : α →₀ ) :
@[simp]
theorem finsupp.count_to_multiset {α : Type u_1} [decidable_eq α] (f : α →₀ ) (a : α) :
= f a
@[simp]
theorem finsupp.mem_to_multiset {α : Type u_1} (f : α →₀ ) (i : α) :
noncomputable def multiset.to_finsupp {α : Type u_1} :

Given a multiset s, s.to_finsupp returns the finitely supported function on ℕ given by the multiplicities of the elements of s.

Equations
@[simp]
theorem multiset.to_finsupp_support {α : Type u_1} [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.to_finsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
=
theorem multiset.to_finsupp_zero {α : Type u_1} :
theorem multiset.to_finsupp_add {α : Type u_1} (s t : multiset α) :
@[simp]
theorem multiset.to_finsupp_singleton {α : Type u_1} (a : α) :
@[simp]
theorem multiset.to_finsupp_to_multiset {α : Type u_1} (s : multiset α) :
theorem multiset.to_finsupp_eq_iff {α : Type u_1} {s : multiset α} {f : α →₀ } :
@[simp]
theorem finsupp.to_multiset_to_finsupp {α : Type u_1} (f : α →₀ ) :

### As an order isomorphism #

noncomputable def finsupp.order_iso_multiset {ι : Type u_3} :

finsupp.to_multiset as an order isomorphism.

Equations
@[simp]
theorem finsupp.coe_order_iso_multiset {ι : Type u_3} :
@[simp]
theorem finsupp.coe_order_iso_multiset_symm {ι : Type u_3} :
theorem finsupp.to_multiset_strict_mono {ι : Type u_3} :
theorem finsupp.sum_id_lt_of_lt {ι : Type u_3} (m n : ι →₀ ) (h : m < n) :
m.sum (λ (_x : ι), id) < n.sum (λ (_x : ι), id)
theorem finsupp.lt_wf (ι : Type u_3) :

The order on ι →₀ ℕ is well-founded.

theorem multiset.to_finsupp_strict_mono {ι : Type u_3} :