Equivalence between Multiset
and ℕ
-valued finitely supported functions #
This defines DFinsupp.toMultiset
the equivalence between Π₀ a : α, ℕ
and Multiset α
, along
with Multiset.toDFinsupp
the reverse equivalence.
instance
DFinsupp.addZeroClass'
{α : Type u_1}
{β : Type u_3}
[AddZeroClass β]
:
AddZeroClass (Π₀ (x : α), β)
Non-dependent special case of DFinsupp.addZeroClass
to help typeclass search.
A DFinsupp version of Finsupp.toMultiset
.
Instances For
@[simp]
theorem
DFinsupp.toMultiset_single
{α : Type u_1}
[DecidableEq α]
(a : α)
(n : ℕ)
:
↑DFinsupp.toMultiset (DFinsupp.single a n) = Multiset.replicate n a
A DFinsupp version of Multiset.toFinsupp
.
Instances For
@[simp]
theorem
Multiset.toDFinsupp_apply
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(a : α)
:
↑(↑Multiset.toDFinsupp s) a = Multiset.count a s
@[simp]
theorem
Multiset.toDFinsupp_support
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
:
DFinsupp.support (↑Multiset.toDFinsupp s) = Multiset.toFinset s
@[simp]
theorem
Multiset.toDFinsupp_replicate
{α : Type u_1}
[DecidableEq α]
(a : α)
(n : ℕ)
:
↑Multiset.toDFinsupp (Multiset.replicate n a) = DFinsupp.single a n
@[simp]
theorem
Multiset.toDFinsupp_singleton
{α : Type u_1}
[DecidableEq α]
(a : α)
:
↑Multiset.toDFinsupp {a} = DFinsupp.single a 1
@[simp]
theorem
Multiset.equivDFinsupp_symm_apply
{α : Type u_1}
[DecidableEq α]
(a : Π₀ (x : α), ℕ)
:
↑(AddEquiv.symm Multiset.equivDFinsupp) a = ↑DFinsupp.toMultiset a
@[simp]
theorem
Multiset.equivDFinsupp_apply
{α : Type u_1}
[DecidableEq α]
(a : Multiset α)
:
↑Multiset.equivDFinsupp a = ↑Multiset.toDFinsupp a
Multiset.toDFinsupp
as an AddEquiv
.
Instances For
@[simp]
theorem
Multiset.toDFinsupp_toMultiset
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
:
↑DFinsupp.toMultiset (↑Multiset.toDFinsupp s) = s
theorem
Multiset.toDFinsupp_injective
{α : Type u_1}
[DecidableEq α]
:
Function.Injective ↑Multiset.toDFinsupp
@[simp]
@[simp]
theorem
Multiset.toDFinsupp_le_toDFinsupp
{α : Type u_1}
[DecidableEq α]
{s : Multiset α}
{t : Multiset α}
:
@[simp]
theorem
Multiset.toDFinsupp_lt_toDFinsupp
{α : Type u_1}
[DecidableEq α]
{s : Multiset α}
{t : Multiset α}
:
@[simp]
theorem
Multiset.toDFinsupp_inter
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
@[simp]
theorem
Multiset.toDFinsupp_union
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
(t : Multiset α)
:
@[simp]
theorem
DFinsupp.toMultiset_toDFinsupp
{α : Type u_1}
[DecidableEq α]
(f : Π₀ (x : α), ℕ)
:
↑Multiset.toDFinsupp (↑DFinsupp.toMultiset f) = f
theorem
DFinsupp.toMultiset_injective
{α : Type u_1}
[DecidableEq α]
:
Function.Injective ↑DFinsupp.toMultiset
@[simp]
theorem
DFinsupp.toMultiset_inj
{α : Type u_1}
[DecidableEq α]
{f : Π₀ (_a : α), ℕ}
{g : Π₀ (_a : α), ℕ}
:
@[simp]
theorem
DFinsupp.toMultiset_le_toMultiset
{α : Type u_1}
[DecidableEq α]
{f : Π₀ (_a : α), ℕ}
{g : Π₀ (_a : α), ℕ}
:
@[simp]
theorem
DFinsupp.toMultiset_lt_toMultiset
{α : Type u_1}
[DecidableEq α]
{f : Π₀ (_a : α), ℕ}
{g : Π₀ (_a : α), ℕ}
:
@[simp]
theorem
DFinsupp.toMultiset_inf
{α : Type u_1}
[DecidableEq α]
(f : Π₀ (_a : α), ℕ)
(g : Π₀ (_a : α), ℕ)
:
@[simp]
theorem
DFinsupp.toMultiset_sup
{α : Type u_1}
[DecidableEq α]
(f : Π₀ (_a : α), ℕ)
(g : Π₀ (_a : α), ℕ)
: