mathlib3 documentation

data.finsupp.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 finsupp.to_multiset the equivalence between α →₀ ℕ and multiset α, along with multiset.to_finsupp the reverse equivalence and finsupp.order_iso_multiset the equivalence promoted to an order isomorphism.

noncomputable def finsupp.to_multiset {α : Type u_1} :

(α →₀ ℕ) ≃+ multiset α

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

Equations

finsupp.to_multiset = {to_fun := λ (f : α →₀ ℕ), f.sum (λ (a : α) (n : ℕ), n • {a}), inv_fun := λ (s : multiset α), {support := s.to_finset, to_fun := λ (a : α), multiset.count a s, mem_support_to_fun := _}, left_inv := _, right_inv := _, map_add' := _}

theorem finsupp.to_multiset_zero {α : Type u_1} :

⇑finsupp.to_multiset 0 = 0

theorem finsupp.to_multiset_add {α : Type u_1} (m n : α →₀ ℕ) :

⇑finsupp.to_multiset (m + n) = ⇑finsupp.to_multiset m + ⇑finsupp.to_multiset n

theorem finsupp.to_multiset_apply {α : Type u_1} (f : α →₀ ℕ) :

⇑finsupp.to_multiset f = f.sum (λ (a : α) (n : ℕ), n • {a})

@[simp]

theorem finsupp.to_multiset_symm_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (x : α) :

⇑(⇑(finsupp.to_multiset.symm) s) x = multiset.count x s

@[simp]

theorem finsupp.to_multiset_single {α : Type u_1} (a : α) (n : ℕ) :

⇑finsupp.to_multiset (finsupp.single a n) = n • {a}

theorem finsupp.to_multiset_sum {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ ℕ} (s : finset ι) :

⇑finsupp.to_multiset (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑finsupp.to_multiset (f i))

theorem finsupp.to_multiset_sum_single {ι : Type u_3} (s : finset ι) (n : ℕ) :

⇑finsupp.to_multiset (s.sum (λ (i : ι), finsupp.single i n)) = n • s.val

theorem finsupp.card_to_multiset {α : Type u_1} (f : α →₀ ℕ) :

⇑multiset.card (⇑finsupp.to_multiset f) = f.sum (λ (a : α), id)

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

multiset.map g (⇑finsupp.to_multiset f) = ⇑finsupp.to_multiset (finsupp.map_domain g f)

@[simp]

theorem finsupp.prod_to_multiset {α : Type u_1} [comm_monoid α] (f : α →₀ ℕ) :

(⇑finsupp.to_multiset f).prod = f.prod (λ (a : α) (n : ℕ), a ^ n)

@[simp]

theorem finsupp.to_finset_to_multiset {α : Type u_1} [decidable_eq α] (f : α →₀ ℕ) :

(⇑finsupp.to_multiset f).to_finset = f.support

@[simp]

theorem finsupp.count_to_multiset {α : Type u_1} [decidable_eq α] (f : α →₀ ℕ) (a : α) :

multiset.count a (⇑finsupp.to_multiset f) = ⇑f a

@[simp]

theorem finsupp.mem_to_multiset {α : Type u_1} (f : α →₀ ℕ) (i : α) :

i ∈ ⇑finsupp.to_multiset f ↔ i ∈ f.support

noncomputable def multiset.to_finsupp {α : Type u_1} :

multiset α ≃+ (α →₀ ℕ)

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

Equations

multiset.to_finsupp = finsupp.to_multiset.symm

@[simp]

theorem multiset.to_finsupp_support {α : Type u_1} [decidable_eq α] (s : multiset α) :

(⇑multiset.to_finsupp s).support = s.to_finset

@[simp]

theorem multiset.to_finsupp_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :

⇑(⇑multiset.to_finsupp s) a = multiset.count a s

theorem multiset.to_finsupp_zero {α : Type u_1} :

⇑multiset.to_finsupp 0 = 0

theorem multiset.to_finsupp_add {α : Type u_1} (s t : multiset α) :

⇑multiset.to_finsupp (s + t) = ⇑multiset.to_finsupp s + ⇑multiset.to_finsupp t

@[simp]

theorem multiset.to_finsupp_singleton {α : Type u_1} (a : α) :

⇑multiset.to_finsupp {a} = finsupp.single a 1

@[simp]

theorem multiset.to_finsupp_to_multiset {α : Type u_1} (s : multiset α) :

⇑finsupp.to_multiset (⇑multiset.to_finsupp s) = s

theorem multiset.to_finsupp_eq_iff {α : Type u_1} {s : multiset α} {f : α →₀ ℕ} :

⇑multiset.to_finsupp s = f ↔ s = ⇑finsupp.to_multiset f

@[simp]

theorem finsupp.to_multiset_to_finsupp {α : Type u_1} (f : α →₀ ℕ) :

⇑multiset.to_finsupp (⇑finsupp.to_multiset f) = f

As an order isomorphism #

noncomputable def finsupp.order_iso_multiset {ι : Type u_3} :

(ι →₀ ℕ) ≃o multiset ι

finsupp.to_multiset as an order isomorphism.

Equations

finsupp.order_iso_multiset = {to_equiv := finsupp.to_multiset.to_equiv, map_rel_iff' := _}

@[simp]

theorem finsupp.coe_order_iso_multiset {ι : Type u_3} :

⇑finsupp.order_iso_multiset = ⇑finsupp.to_multiset

@[simp]

theorem finsupp.coe_order_iso_multiset_symm {ι : Type u_3} :

⇑(finsupp.order_iso_multiset.symm) = ⇑multiset.to_finsupp

theorem finsupp.to_multiset_strict_mono {ι : Type u_3} :

strict_mono ⇑finsupp.to_multiset

theorem finsupp.sum_id_lt_of_lt {ι : Type u_3} (m n : ι →₀ ℕ) (h : m < n) :

m.sum (λ (_x : ι), id) < n.sum (λ (_x : ι), id)

theorem finsupp.lt_wf (ι : Type u_3) :

well_founded has_lt.lt

The order on ι →₀ ℕ is well-founded.

theorem multiset.to_finsupp_strict_mono {ι : Type u_3} :

strict_mono ⇑multiset.to_finsupp