mathlib3 documentation

data.dfinsupp.multiset

Equivalence between multiset and ℕ-valued finitely supported functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines dfinsupp.to_multiset the equivalence between Π₀ a : α, ℕ and multiset α, along with multiset.to_dfinsupp the reverse equivalence.

Note that this provides a computable alternative to finsupp.to_multiset.

source
@[protected, instance]
def dfinsupp.add_zero_class' {α : Type u_1} {β : Type u_2} [add_zero_class β] :
add_zero_class (Π₀ (a : α), β)

Non-dependent special case of dfinsupp.add_zero_class to help typeclass search.

Equations
source
def dfinsupp.to_multiset {α : Type u_1} [decidable_eq α] :
(Π₀ (a : α), ℕ) →+ multiset α

A computable version of finsupp.to_multiset.

Equations
source
@[simp]
theorem dfinsupp.to_multiset_single {α : Type u_1} [decidable_eq α] (a : α) (n : ℕ) :
⇑dfinsupp.to_multiset (dfinsupp.single a n) = multiset.replicate n a
source
def multiset.to_dfinsupp {α : Type u_1} [decidable_eq α] :
multiset α →+ Π₀ (a : α), ℕ

A computable version of multiset.to_finsupp

Equations
source
@[simp]
theorem multiset.to_dfinsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
⇑(⇑multiset.to_dfinsupp s) a = multiset.count a s
source
@[simp]
theorem multiset.to_dfinsupp_support {α : Type u_1} [decidable_eq α] (s : multiset α) :
(⇑multiset.to_dfinsupp s).support = s.to_finset
source
@[simp]
theorem multiset.to_dfinsupp_replicate {α : Type u_1} [decidable_eq α] (a : α) (n : ℕ) :
⇑multiset.to_dfinsupp (multiset.replicate n a) = dfinsupp.single a n
source
@[simp]
theorem multiset.to_dfinsupp_singleton {α : Type u_1} [decidable_eq α] (a : α) :
⇑multiset.to_dfinsupp {a} = dfinsupp.single a 1
source
def multiset.equiv_dfinsupp {α : Type u_1} [decidable_eq α] :
multiset α ≃+ Π₀ (a : α), ℕ

multiset.to_dfinsupp as an add_equiv.

Equations
source
@[simp]
theorem multiset.equiv_dfinsupp_apply {α : Type u_1} [decidable_eq α] (ᾰ : multiset α) :
⇑multiset.equiv_dfinsupp ᾰ = ⇑multiset.to_dfinsupp ᾰ
source
@[simp]
theorem multiset.equiv_dfinsupp_symm_apply {α : Type u_1} [decidable_eq α] (ᾰ : Π₀ (a : α), ℕ) :
⇑(multiset.equiv_dfinsupp.symm) ᾰ = ⇑dfinsupp.to_multiset ᾰ
source
@[simp]
theorem multiset.to_dfinsupp_to_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) :
⇑dfinsupp.to_multiset (⇑multiset.to_dfinsupp s) = s
source
theorem multiset.to_dfinsupp_injective {α : Type u_1} [decidable_eq α] :
function.injective ⇑multiset.to_dfinsupp
source
@[simp]
theorem multiset.to_dfinsupp_inj {α : Type u_1} [decidable_eq α] {s t : multiset α} :
⇑multiset.to_dfinsupp s = ⇑multiset.to_dfinsupp t ↔ s = t
source
@[simp]
theorem multiset.to_dfinsupp_le_to_dfinsupp {α : Type u_1} [decidable_eq α] {s t : multiset α} :
⇑multiset.to_dfinsupp s ≤ ⇑multiset.to_dfinsupp t ↔ s ≤ t
source
@[simp]
theorem multiset.to_dfinsupp_lt_to_dfinsupp {α : Type u_1} [decidable_eq α] {s t : multiset α} :
⇑multiset.to_dfinsupp s < ⇑multiset.to_dfinsupp t ↔ s < t
source
@[simp]
theorem multiset.to_dfinsupp_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
⇑multiset.to_dfinsupp (s ∩ t) = ⇑multiset.to_dfinsupp s ⊓ ⇑multiset.to_dfinsupp t
source
@[simp]
theorem multiset.to_dfinsupp_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :
⇑multiset.to_dfinsupp (s ∪ t) = ⇑multiset.to_dfinsupp s ⊔ ⇑multiset.to_dfinsupp t
source
@[simp]
theorem dfinsupp.to_multiset_to_dfinsupp {α : Type u_1} [decidable_eq α] {f : Π₀ (a : α), ℕ} :
⇑multiset.to_dfinsupp (⇑dfinsupp.to_multiset f) = f
source
theorem dfinsupp.to_multiset_injective {α : Type u_1} [decidable_eq α] :
function.injective ⇑dfinsupp.to_multiset
source
@[simp]
theorem dfinsupp.to_multiset_inj {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), ℕ} :
⇑dfinsupp.to_multiset f = ⇑dfinsupp.to_multiset g ↔ f = g
source
@[simp]
theorem dfinsupp.to_multiset_le_to_multiset {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), ℕ} :
⇑dfinsupp.to_multiset f ≤ ⇑dfinsupp.to_multiset g ↔ f ≤ g
source
@[simp]
theorem dfinsupp.to_multiset_lt_to_multiset {α : Type u_1} [decidable_eq α] {f g : Π₀ (a : α), ℕ} :
⇑dfinsupp.to_multiset f < ⇑dfinsupp.to_multiset g ↔ f < g
source
@[simp]
theorem dfinsupp.to_multiset_inf {α : Type u_1} [decidable_eq α] (f g : Π₀ (a : α), ℕ) :
⇑dfinsupp.to_multiset (f ⊓ g) = ⇑dfinsupp.to_multiset f ∩ ⇑dfinsupp.to_multiset g
source
@[simp]
theorem dfinsupp.to_multiset_sup {α : Type u_1} [decidable_eq α] (f g : Π₀ (a : α), ℕ) :
⇑dfinsupp.to_multiset (f ⊔ g) = ⇑dfinsupp.to_multiset f ∪ ⇑dfinsupp.to_multiset g