Multiset coercion to type

This module defines a CoeSort instance for multisets and gives it a Fintype instance. It also defines Multiset.toEnumFinset, which is another way to enumerate the elements of a multiset. These coercions and definitions make it easier to sum over multisets using existing Finset theory.

Main definitions

• A coercion from m : Multiset α to a Type*. Each x : m has two components. The first, x.1, can be obtained via the coercion ↑x : α, and it yields the underlying element of the multiset. The second, x.2, is a term of Fin (m.count x), and its function is to ensure each term appears with the correct multiplicity. Note that this coercion requires DecidableEq α due to the definition using Multiset.count.
• Multiset.toEnumFinset is a Finset version of this.
• Multiset.coeEmbedding is the embedding m ↪ α × ℕ, whose first component is the coercion and whose second component enumerates elements with multiplicity.
• Multiset.coeEquiv is the equivalence m ≃ m.toEnumFinset.

Tags

multiset enumeration

def Multiset.ToType {α : Type u_1} [DecidableEq α] (m : Multiset α) : Type u_1

Auxiliary definition for the CoeSort instance. This prevents the CoeOut m α instance from inadvertently applying to other sigma types.

Equations

• m.ToType = ((x : α) × Fin (Multiset.count x m))

instance instCoeSortMultisetType {α : Type u_1} [DecidableEq α] : CoeSort (Multiset α) (Type u_1)

Create a type that has the same number of elements as the multiset. Terms of this type are triples ⟨x, ⟨i, h⟩⟩ where x : α, i : ℕ, and h : i < m.count x. This way repeated elements of a multiset appear multiple times from different values of i.

Equations

• instCoeSortMultisetType = { coe := Multiset.ToType }

@[reducible, match_pattern]

def Multiset.mkToType {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : α) (i : Fin (Multiset.count x m)) : m.ToType

Constructor for terms of the coercion of m to a type. This helps Lean pick up the correct instances.

Equations

• m.mkToType x i = ⟨x, i⟩

instance instCoeSortMultisetType.instCoeOutToType {α : Type u_1} [DecidableEq α] {m : Multiset α} : CoeOut m.ToType α

As a convenience, there is a coercion from m : Type* to α by projecting onto the first component.

Equations

• instCoeSortMultisetType.instCoeOutToType = { coe := fun (x : m.ToType) => x.fst }

theorem Multiset.coe_mk {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : α} {i : Fin (Multiset.count x m)} : (m.mkToType x i).fst = x

@[simp]

theorem Multiset.coe_mem {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : m.ToType} : x.fst ∈ m

@[simp]

theorem Multiset.forall_coe {α : Type u_1} [DecidableEq α] {m : Multiset α} (p : m.ToType → Prop) : (∀ (x : m.ToType), p x) ↔ ∀ (x : α) (i : Fin (Multiset.count x m)), p ⟨x, i⟩

@[simp]

theorem Multiset.exists_coe {α : Type u_1} [DecidableEq α] {m : Multiset α} (p : m.ToType → Prop) : (∃ (x : m.ToType), p x) ↔ ∃ (x : α) (i : Fin (Multiset.count x m)), p ⟨x, i⟩

instance instFintypeElemProdNatSetOfLtSndCountFst {α : Type u_1} [DecidableEq α] {m : Multiset α} : Fintype ↑{p : α × ℕ | p.2 < Multiset.count p.1 m}

Equations

• instFintypeElemProdNatSetOfLtSndCountFst = Fintype.ofFinset (m.toFinset.biUnion fun (x : α) => Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (Multiset.count x m))) ⋯

def Multiset.toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) : Finset (α × ℕ)

Construct a finset whose elements enumerate the elements of the multiset m. The ℕ component is used to differentiate between equal elements: if x appears n times then (x, 0), ..., and (x, n-1) appear in the Finset.

Equations

• m.toEnumFinset = {p : α × ℕ | p.2 < Multiset.count p.1 m}.toFinset

@[simp]

theorem Multiset.mem_toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) (p : α × ℕ) : p ∈ m.toEnumFinset ↔ p.2 < Multiset.count p.1 m

theorem Multiset.mem_of_mem_toEnumFinset {α : Type u_1} [DecidableEq α] {m : Multiset α} {p : α × ℕ} (h : p ∈ m.toEnumFinset) : p.1 ∈ m

@[simp]

theorem Multiset.toEnumFinset_filter_eq {α : Type u_1} [DecidableEq α] (m : Multiset α) (a : α) : Finset.filter (fun (x : α × ℕ) => x.1 = a) m.toEnumFinset = {a} ×ˢ Finset.range (Multiset.count a m)

@[simp]

theorem Multiset.map_toEnumFinset_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) : Multiset.map Prod.fst m.toEnumFinset.val = m

@[simp]

theorem Multiset.image_toEnumFinset_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) : Finset.image Prod.fst m.toEnumFinset = m.toFinset

@[simp]

theorem Multiset.map_fst_le_of_subset_toEnumFinset {α : Type u_1} [DecidableEq α] {m : Multiset α} {s : Finset (α × ℕ)} (hsm : s ⊆ m.toEnumFinset) : Multiset.map Prod.fst s.val ≤ m

theorem Multiset.toEnumFinset_mono {α : Type u_1} [DecidableEq α] {m₁ : Multiset α} {m₂ : Multiset α} (h : m₁ ≤ m₂) : m₁.toEnumFinset ⊆ m₂.toEnumFinset

@[simp]

theorem Multiset.toEnumFinset_subset_iff {α : Type u_1} [DecidableEq α] {m₁ : Multiset α} {m₂ : Multiset α} : m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂

@[simp]

theorem Multiset.coeEmbedding_apply {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) : m.coeEmbedding x = (x.fst, ↑x.snd)

def Multiset.coeEmbedding {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.ToType ↪ α × ℕ

The embedding from a multiset into α × ℕ where the second coordinate enumerates repeats. If you are looking for the function m → α, that would be plain (↑).

Equations

• m.coeEmbedding = { toFun := fun (x : m.ToType) => (x.fst, ↑x.snd), inj' := ⋯ }

@[simp]

theorem Multiset.coeEquiv_symm_apply_fst {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : { x : α × ℕ // x ∈ m.toEnumFinset }) : (m.coeEquiv.symm x).fst = (↑x).1

@[simp]

theorem Multiset.coeEquiv_apply_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) : ↑(m.coeEquiv x) = m.coeEmbedding x

@[simp]

theorem Multiset.coeEquiv_symm_apply_snd_val {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : { x : α × ℕ // x ∈ m.toEnumFinset }) : ↑(m.coeEquiv.symm x).snd = (↑x).2

def Multiset.coeEquiv {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.ToType ≃ { x : α × ℕ // x ∈ m.toEnumFinset }

Another way to coerce a Multiset to a type is to go through m.toEnumFinset and coerce that Finset to a type.

Equations

• m.coeEquiv = { toFun := fun (x : m.ToType) => ⟨m.coeEmbedding x, ⋯⟩, invFun := fun (x : { x : α × ℕ // x ∈ m.toEnumFinset }) => ⟨(↑x).1, ⟨(↑x).2, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Multiset.toEmbedding_coeEquiv_trans {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun (x : α × ℕ) => x ∈ m.toEnumFinset) = m.coeEmbedding

@[irreducible]

instance Multiset.fintypeCoe {α : Type u_1} [DecidableEq α] {m : Multiset α} : Fintype m.ToType

Equations

• Multiset.fintypeCoe = Fintype.ofEquiv { x : α × ℕ // x ∈ m.toEnumFinset } m.coeEquiv.symm

theorem Multiset.map_univ_coeEmbedding {α : Type u_1} [DecidableEq α] (m : Multiset α) : Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset

@[simp]

theorem Multiset.map_univ_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) : Multiset.map (fun (x : m.ToType) => x.fst) Finset.univ.val = m

@[simp]

theorem Multiset.map_univ {α : Type u_1} [DecidableEq α] {β : Type u_2} (m : Multiset α) (f : α → β) : Multiset.map (fun (x : m.ToType) => f x.fst) Finset.univ.val = Multiset.map f m

@[simp]

theorem Multiset.card_toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.toEnumFinset.card = Multiset.card m

@[simp]

theorem Multiset.card_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) : Fintype.card m.ToType = Multiset.card m

theorem Multiset.sum_eq_sum_coe {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) : m.sum = ∑ x : m.ToType, x.fst

theorem Multiset.prod_eq_prod_coe {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) : m.prod = ∏ x : m.ToType, x.fst

theorem Multiset.sum_eq_sum_toEnumFinset {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) : m.sum = ∑ x ∈ m.toEnumFinset, x.1

theorem Multiset.prod_eq_prod_toEnumFinset {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) : m.prod = ∏ x ∈ m.toEnumFinset, x.1

theorem Multiset.sum_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] (m : Multiset α) (f : α → ℕ → β) : ∑ x ∈ m.toEnumFinset, f x.1 x.2 = ∑ x : m.ToType, f x.fst ↑x.snd

theorem Multiset.prod_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [CommMonoid β] (m : Multiset α) (f : α → ℕ → β) : ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m.ToType, f x.fst ↑x.snd