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

def DFinsupp.toMultiset {α : Type u_1} [DecidableEq α] : (Π₀ (x : α), ℕ) →+ Multiset α

A DFinsupp version of Finsupp.toMultiset.

Equations

• DFinsupp.toMultiset = DFinsupp.sumAddHom fun (a : α) => Multiset.replicateAddMonoidHom a

@[simp]

theorem DFinsupp.toMultiset_single {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : toMultiset (single a n) = Multiset.replicate n a

def Multiset.toDFinsupp {α : Type u_1} [DecidableEq α] : Multiset α →+ Π₀ (x : α), ℕ

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' := ⋯ }

@[simp]

theorem Multiset.toDFinsupp_apply {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : (toDFinsupp s) a = count a s

@[simp]

theorem Multiset.toDFinsupp_support {α : Type u_1} [DecidableEq α] (s : Multiset α) : (toDFinsupp s).support = s.toFinset

@[simp]

theorem Multiset.toDFinsupp_replicate {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : toDFinsupp (replicate n a) = DFinsupp.single a n

@[simp]

theorem Multiset.toDFinsupp_singleton {α : Type u_1} [DecidableEq α] (a : α) : toDFinsupp {a} = DFinsupp.single a 1

def Multiset.equivDFinsupp {α : Type u_1} [DecidableEq α] : Multiset α ≃+ Π₀ (x : α), ℕ

Multiset.toDFinsupp as an AddEquiv.

Equations

• Multiset.equivDFinsupp = Multiset.toDFinsupp.toAddEquiv DFinsupp.toMultiset ⋯ ⋯

@[simp]

theorem Multiset.equivDFinsupp_symm_apply {α : Type u_1} [DecidableEq α] (a : Π₀ (x : α), ℕ) : equivDFinsupp.symm a = DFinsupp.toMultiset a

@[simp]

theorem Multiset.equivDFinsupp_apply {α : Type u_1} [DecidableEq α] (a : Multiset α) : equivDFinsupp a = toDFinsupp a

@[simp]

theorem Multiset.toDFinsupp_toMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) : DFinsupp.toMultiset (toDFinsupp s) = s

theorem Multiset.toDFinsupp_injective {α : Type u_1} [DecidableEq α] : Function.Injective ⇑toDFinsupp

@[simp]

theorem Multiset.toDFinsupp_inj {α : Type u_1} [DecidableEq α] {s t : Multiset α} : toDFinsupp s = toDFinsupp t ↔ s = t

@[simp]

theorem Multiset.toDFinsupp_le_toDFinsupp {α : Type u_1} [DecidableEq α] {s t : Multiset α} : toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t

@[simp]

theorem Multiset.toDFinsupp_lt_toDFinsupp {α : Type u_1} [DecidableEq α] {s t : Multiset α} : toDFinsupp s < toDFinsupp t ↔ s < t

@[simp]

theorem Multiset.toDFinsupp_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

@[simp]

theorem Multiset.toDFinsupp_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) : toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

@[simp]

theorem DFinsupp.toMultiset_toDFinsupp {α : Type u_1} [DecidableEq α] (f : Π₀ (x : α), ℕ) : Multiset.toDFinsupp (toMultiset f) = f

theorem DFinsupp.toMultiset_injective {α : Type u_1} [DecidableEq α] : Function.Injective ⇑toMultiset

@[simp]

theorem DFinsupp.toMultiset_inj {α : Type u_1} [DecidableEq α] {f g : Π₀ (_a : α), ℕ} : toMultiset f = toMultiset g ↔ f = g

@[simp]

theorem DFinsupp.toMultiset_le_toMultiset {α : Type u_1} [DecidableEq α] {f g : Π₀ (_a : α), ℕ} : toMultiset f ≤ toMultiset g ↔ f ≤ g

@[simp]

theorem DFinsupp.toMultiset_lt_toMultiset {α : Type u_1} [DecidableEq α] {f g : Π₀ (_a : α), ℕ} : toMultiset f < toMultiset g ↔ f < g

@[simp]

theorem DFinsupp.toMultiset_inf {α : Type u_1} [DecidableEq α] (f g : Π₀ (_a : α), ℕ) : toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g

@[simp]

theorem DFinsupp.toMultiset_sup {α : Type u_1} [DecidableEq α] (f g : Π₀ (_a : α), ℕ) : toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g