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_2}
[AddZeroClass β]
:
AddZeroClass (Π₀ (x : α), β)
Non-dependent special case of DFinsupp.addZeroClass
to help typeclass search.
Equations
- DFinsupp.addZeroClass' = DFinsupp.addZeroClass
A DFinsupp version of Finsupp.toMultiset
.
Equations
- DFinsupp.toMultiset = DFinsupp.sumAddHom fun (a : α) => Multiset.replicateAddMonoidHom a
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
.
Equations
- Multiset.toDFinsupp = { toFun := fun (s : Multiset α) => { toFun := fun (n : α) => Multiset.count n s, support' := Trunc.mk ⟨s, ⋯⟩ }, map_zero' := ⋯, map_add' := ⋯ }
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 α)
:
(Multiset.toDFinsupp s).support = s.toFinset
@[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 : α), ℕ)
:
Multiset.equivDFinsupp.symm 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
.
Equations
- Multiset.equivDFinsupp = Multiset.toDFinsupp.toAddEquiv DFinsupp.toMultiset ⋯ ⋯
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 : α), ℕ)
: