mathlib documentation

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_apply {α : Type u_1} (f : α →₀ ) :
finsupp.to_multiset 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 : ) :
theorem finsupp.to_multiset_sum {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ } (s : finset ι) :
finsupp.to_multiset (∑ (i : ι) in s, f i) = ∑ (i : ι) in s, finsupp.to_multiset (f i)
theorem finsupp.to_multiset_sum_single {ι : Type u_3} (s : finset ι) (n : ) :
finsupp.to_multiset (∑ (i : ι) in s, finsupp.single i n) = n s.val
theorem finsupp.card_to_multiset {α : Type u_1} (f : α →₀ ) :
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 : α →₀ ) :
(finsupp.to_multiset f).prod = f.prod (λ (a : α) (n : ), a ^ n)
@[simp]
@[simp]
theorem finsupp.count_to_multiset {α : Type u_1} [decidable_eq α] (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]
@[simp]
theorem multiset.to_finsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
theorem multiset.to_finsupp_zero {α : Type u_1} :
@[simp]
theorem multiset.to_finsupp_singleton {α : Type u_1} (a : α) :

As an order isomorphism #

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

finsupp.to_multiset as an order isomorphism.

Equations
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.