Equivalence between `Multiset` and `ℕ`-valued finitely supported functions #

This defines Finsupp.toMultiset the equivalence between α →₀ ℕ and Multiset α, along with Multiset.toFinsupp the reverse equivalence and Finsupp.orderIsoMultiset the equivalence promoted to an order isomorphism.

source

def Finsupp.toMultiset {α : Type u_1} :

(α →₀ ℕ) →+ Multiset α

Given f : α →₀ ℕ, f.toMultiset is the multiset with multiplicities given by the values of f on the elements of α. We define this function as an AddMonoidHom.

Under the additional assumption of [DecidableEq α], this is available as Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ); the two declarations are separate as this assumption is only needed for one direction.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Finsupp.toMultiset_zero {α : Type u_1} :

↑Finsupp.toMultiset 0 = 0

source

theorem Finsupp.toMultiset_add {α : Type u_1} (m : α →₀ ℕ) (n : α →₀ ℕ) :

↑Finsupp.toMultiset (m + n) = ↑Finsupp.toMultiset m + ↑Finsupp.toMultiset n

source

theorem Finsupp.toMultiset_apply {α : Type u_1} (f : α →₀ ℕ) :

↑Finsupp.toMultiset f = Finsupp.sum f fun a n => n • {a}

source

@[simp]

theorem Finsupp.toMultiset_single {α : Type u_1} (a : α) (n : ℕ) :

(↑Finsupp.toMultiset fun₀ | a => n) = n • {a}

source

theorem Finsupp.toMultiset_sum {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ ℕ} (s : Finset ι) :

↑Finsupp.toMultiset (Finset.sum s fun i => f i) = Finset.sum s fun i => ↑Finsupp.toMultiset (f i)

source

theorem Finsupp.toMultiset_sum_single {ι : Type u_3} (s : Finset ι) (n : ℕ) :

↑Finsupp.toMultiset (Finset.sum s fun i => fun₀ | i => n) = n • s.val

source

theorem Finsupp.card_toMultiset {α : Type u_1} (f : α →₀ ℕ) :

↑Multiset.card (↑Finsupp.toMultiset f) = Finsupp.sum f fun x => id

source

theorem Finsupp.toMultiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ℕ) (g : α → β) :

Multiset.map g (↑Finsupp.toMultiset f) = ↑Finsupp.toMultiset (Finsupp.mapDomain g f)

source

@[simp]

theorem Finsupp.sum_toMultiset {α : Type u_1} [AddCommMonoid α] (f : α →₀ ℕ) :

Multiset.sum (↑Finsupp.toMultiset f) = Finsupp.sum f fun a n => n • a

source

@[simp]

theorem Finsupp.prod_toMultiset {α : Type u_1} [CommMonoid α] (f : α →₀ ℕ) :

Multiset.prod (↑Finsupp.toMultiset f) = Finsupp.prod f fun a n => a ^ n

source

@[simp]

theorem Finsupp.toFinset_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) :

Multiset.toFinset (↑Finsupp.toMultiset f) = f.support

source

@[simp]

theorem Finsupp.count_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (a : α) :

Multiset.count a (↑Finsupp.toMultiset f) = ↑f a

source

theorem Finsupp.toMultiset_sup {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) :

↑Finsupp.toMultiset (f ⊔ g) = ↑Finsupp.toMultiset f ∪ ↑Finsupp.toMultiset g

source

theorem Finsupp.toMultiset_inf {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) :

↑Finsupp.toMultiset (f ⊓ g) = ↑Finsupp.toMultiset f ∩ ↑Finsupp.toMultiset g

source

@[simp]

theorem Finsupp.mem_toMultiset {α : Type u_1} (f : α →₀ ℕ) (i : α) :

i ∈ ↑Finsupp.toMultiset f ↔ i ∈ f.support

source

@[simp]

theorem Multiset.toFinsupp_symm_apply {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) :

↑(AddEquiv.symm Multiset.toFinsupp) f = ↑Finsupp.toMultiset f

source

def Multiset.toFinsupp {α : Type u_1} [DecidableEq α] :

Multiset α ≃+ (α →₀ ℕ)

Given a multiset s, s.toFinsupp returns the finitely supported function on ℕ given by the multiplicities of the elements of s.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Multiset.toFinsupp_support {α : Type u_1} [DecidableEq α] (s : Multiset α) :

(↑Multiset.toFinsupp s).support = Multiset.toFinset s

source

@[simp]

theorem Multiset.toFinsupp_apply {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) :

↑(↑Multiset.toFinsupp s) a = Multiset.count a s

source

theorem Multiset.toFinsupp_zero {α : Type u_1} [DecidableEq α] :

↑Multiset.toFinsupp 0 = 0

source

theorem Multiset.toFinsupp_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

↑Multiset.toFinsupp (s + t) = ↑Multiset.toFinsupp s + ↑Multiset.toFinsupp t

source

@[simp]

theorem Multiset.toFinsupp_singleton {α : Type u_1} [DecidableEq α] (a : α) :

↑Multiset.toFinsupp {a} = fun₀ | a => 1

source

@[simp]

theorem Multiset.toFinsupp_toMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) :

↑Finsupp.toMultiset (↑Multiset.toFinsupp s) = s

source

theorem Multiset.toFinsupp_eq_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {f : α →₀ ℕ} :

↑Multiset.toFinsupp s = f ↔ s = ↑Finsupp.toMultiset f

source

theorem Multiset.toFinsupp_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

↑Multiset.toFinsupp (s ∪ t) = ↑Multiset.toFinsupp s ⊔ ↑Multiset.toFinsupp t

source

theorem Multiset.toFinsupp_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :

↑Multiset.toFinsupp (s ∩ t) = ↑Multiset.toFinsupp s ⊓ ↑Multiset.toFinsupp t

source

@[simp]

theorem Finsupp.toMultiset_toFinsupp {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) :

↑Multiset.toFinsupp (↑Finsupp.toMultiset f) = f

source

theorem Finsupp.toMultiset_eq_iff {α : Type u_1} [DecidableEq α] {f : α →₀ ℕ} {s : Multiset α} :

↑Finsupp.toMultiset f = s ↔ f = ↑Multiset.toFinsupp s

As an order isomorphism #

source

def Finsupp.orderIsoMultiset {ι : Type u_3} [DecidableEq ι] :

(ι →₀ ℕ) ≃o Multiset ι

Finsupp.toMultiset as an order isomorphism.

Equations

Finsupp.orderIsoMultiset = { toEquiv := (AddEquiv.symm Multiset.toFinsupp).toEquiv, map_rel_iff' := (_ : ∀ {f g : ι →₀ ℕ}, ↑Finsupp.toMultiset f ≤ ↑Finsupp.toMultiset g ↔ f ≤ g) }