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.
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
.
@[simp]
theorem
finsupp.to_multiset_symm_apply
{α : Type u_1}
[decidable_eq α]
(s : multiset α)
(x : α) :
⇑(⇑(finsupp.to_multiset.symm) s) x = multiset.count x s
@[simp]
theorem
finsupp.to_multiset_single
{α : Type u_1}
(a : α)
(n : ℕ) :
⇑finsupp.to_multiset (finsupp.single 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 : ι), finsupp.single i n)) = n • s.val
theorem
finsupp.card_to_multiset
{α : Type u_1}
(f : α →₀ ℕ) :
⇑multiset.card (⇑finsupp.to_multiset f) = f.sum (λ (a : α), id)
@[simp]
@[simp]
@[simp]
theorem
finsupp.count_to_multiset
{α : Type u_1}
[decidable_eq α]
(f : α →₀ ℕ)
(a : α) :
multiset.count a (⇑finsupp.to_multiset f) = ⇑f a
@[simp]
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 : α) :
⇑(⇑multiset.to_finsupp s) a = multiset.count a s
@[simp]
theorem
multiset.to_finsupp_singleton
{α : Type u_1}
(a : α) :
⇑multiset.to_finsupp {a} = finsupp.single a 1
@[simp]
theorem
multiset.to_finsupp_eq_iff
{α : Type u_1}
{s : multiset α}
{f : α →₀ ℕ} :
⇑multiset.to_finsupp s = f ↔ s = ⇑finsupp.to_multiset f
@[simp]
As an order isomorphism #
finsupp.to_multiset
as an order isomorphism.
Equations
@[simp]
@[simp]
The order on ι →₀ ℕ
is well-founded.