# Documentation

Mathlib.Data.Finsupp.Multiset

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

This defines Finsupp.toMultiset the equivalence between α →₀ ℕ and Multiset α, along with Multiset.toFinsupp the reverse equivalence and Finsupp.orderIsoMultiset the equivalence promoted to an order isomorphism.

def Finsupp.toMultiset {α : Type u_1} :

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

Under the additional assumption of [DecidableEq α], this is available as Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ); the two declarations are separate as this assumption is only needed for one direction.

Instances For
theorem Finsupp.toMultiset_zero {α : Type u_1} :
Finsupp.toMultiset 0 = 0
theorem Finsupp.toMultiset_add {α : Type u_1} (m : α →₀ ) (n : α →₀ ) :
Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n
theorem Finsupp.toMultiset_apply {α : Type u_1} (f : α →₀ ) :
Finsupp.toMultiset f = Finsupp.sum f fun a n => n {a}
@[simp]
theorem Finsupp.toMultiset_single {α : Type u_1} (a : α) (n : ) :
(Finsupp.toMultiset fun₀ | a => n) = n {a}
theorem Finsupp.toMultiset_sum {α : Type u_1} {ι : Type u_3} {f : ια →₀ } (s : ) :
Finsupp.toMultiset (Finset.sum s fun i => f i) = Finset.sum s fun i => Finsupp.toMultiset (f i)
theorem Finsupp.toMultiset_sum_single {ι : Type u_3} (s : ) (n : ) :
Finsupp.toMultiset (Finset.sum s fun i => fun₀ | i => n) = n s.val
theorem Finsupp.card_toMultiset {α : Type u_1} (f : α →₀ ) :
Multiset.card (Finsupp.toMultiset f) = Finsupp.sum f fun x => id
theorem Finsupp.toMultiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ) (g : αβ) :
Multiset.map g (Finsupp.toMultiset f) = Finsupp.toMultiset ()
@[simp]
theorem Finsupp.prod_toMultiset {α : Type u_1} [] (f : α →₀ ) :
Multiset.prod (Finsupp.toMultiset f) = Finsupp.prod f fun a n => a ^ n
@[simp]
theorem Finsupp.toFinset_toMultiset {α : Type u_1} [] (f : α →₀ ) :
Multiset.toFinset (Finsupp.toMultiset f) = f.support
@[simp]
theorem Finsupp.count_toMultiset {α : Type u_1} [] (f : α →₀ ) (a : α) :
Multiset.count a (Finsupp.toMultiset f) = f a
theorem Finsupp.toMultiset_sup {α : Type u_1} [] (f : α →₀ ) (g : α →₀ ) :
Finsupp.toMultiset (f g) = Finsupp.toMultiset f Finsupp.toMultiset g
theorem Finsupp.toMultiset_inf {α : Type u_1} [] (f : α →₀ ) (g : α →₀ ) :
Finsupp.toMultiset (f g) = Finsupp.toMultiset f Finsupp.toMultiset g
@[simp]
theorem Finsupp.mem_toMultiset {α : Type u_1} (f : α →₀ ) (i : α) :
i Finsupp.toMultiset f i f.support
@[simp]
theorem Multiset.toFinsupp_symm_apply {α : Type u_1} [] (f : α →₀ ) :
↑(AddEquiv.symm Multiset.toFinsupp) f = Finsupp.toMultiset f
def Multiset.toFinsupp {α : Type u_1} [] :

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

Instances For
@[simp]
theorem Multiset.toFinsupp_support {α : Type u_1} [] (s : ) :
(Multiset.toFinsupp s).support =
@[simp]
theorem Multiset.toFinsupp_apply {α : Type u_1} [] (s : ) (a : α) :
↑(Multiset.toFinsupp s) a =
theorem Multiset.toFinsupp_zero {α : Type u_1} [] :
Multiset.toFinsupp 0 = 0
theorem Multiset.toFinsupp_add {α : Type u_1} [] (s : ) (t : ) :
Multiset.toFinsupp (s + t) = Multiset.toFinsupp s + Multiset.toFinsupp t
@[simp]
theorem Multiset.toFinsupp_singleton {α : Type u_1} [] (a : α) :
Multiset.toFinsupp {a} = fun₀ | a => 1
@[simp]
theorem Multiset.toFinsupp_toMultiset {α : Type u_1} [] (s : ) :
Finsupp.toMultiset (Multiset.toFinsupp s) = s
theorem Multiset.toFinsupp_eq_iff {α : Type u_1} [] {s : } {f : α →₀ } :
Multiset.toFinsupp s = f s = Finsupp.toMultiset f
theorem Multiset.toFinsupp_union {α : Type u_1} [] (s : ) (t : ) :
Multiset.toFinsupp (s t) = Multiset.toFinsupp s Multiset.toFinsupp t
theorem Multiset.toFinsupp_inter {α : Type u_1} [] (s : ) (t : ) :
Multiset.toFinsupp (s t) = Multiset.toFinsupp s Multiset.toFinsupp t
@[simp]
theorem Finsupp.toMultiset_toFinsupp {α : Type u_1} [] (f : α →₀ ) :
Multiset.toFinsupp (Finsupp.toMultiset f) = f
theorem Finsupp.toMultiset_eq_iff {α : Type u_1} [] {f : α →₀ } {s : } :
Finsupp.toMultiset f = s f = Multiset.toFinsupp s

### As an order isomorphism #

def Finsupp.orderIsoMultiset {ι : Type u_3} [] :

Finsupp.toMultiset as an order isomorphism.

Instances For
@[simp]
theorem Finsupp.coe_orderIsoMultiset {ι : Type u_3} [] :
Finsupp.orderIsoMultiset = Finsupp.toMultiset
@[simp]
theorem Finsupp.coe_orderIsoMultiset_symm {ι : Type u_3} [] :
↑(OrderIso.symm Finsupp.orderIsoMultiset) = Multiset.toFinsupp
theorem Finsupp.toMultiset_strictMono {ι : Type u_3} :
StrictMono Finsupp.toMultiset
theorem Finsupp.sum_id_lt_of_lt {ι : Type u_3} (m : ι →₀ ) (n : ι →₀ ) (h : m < n) :
(Finsupp.sum m fun x => id) < Finsupp.sum n fun x => id
theorem Finsupp.lt_wf (ι : Type u_3) :

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

theorem Multiset.toFinsupp_strictMono {ι : Type u_3} [] :
StrictMono Multiset.toFinsupp