Multiset coercion to type

This module defines a hasCoeToSort 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*. For x : m, then there is a coercion ↑x : α, and x.2 is a term of Fin (m.count x). The second component is what ensures each term appears with the correct multiplicity. Note that this coercion requires decidableEq α due to 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 hasCoeToSort instance. This prevents the hasCoe m α instance from inadvertently applying to other sigma types. One should not use this definition directly.

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 with different values of i.

@[match_pattern, reducible]

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

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

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

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

@[simp]

theorem Multiset.coe_eq {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : Multiset.ToType m} {y : Multiset.ToType m} : x.fst = y.fst ↔ x.fst = y.fst

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

@[simp]

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

@[simp]

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

@[simp]

theorem Multiset.exists_coe {α : Type u_1} [DecidableEq α] {m : Multiset α} (p : Multiset.ToType m → Prop) : (∃ x, p x) ↔ ∃ x i, p { fst := x, snd := i }

instance instFintypeElemProdNatSetOfLtInstLTNatSndCountFst {α : Type u_1} [DecidableEq α] {m : Multiset α} : Fintype ↑{p | p.snd < Multiset.count p.fst 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.

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[irreducible]

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

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

theorem Multiset.toEnumFinset_filter_eq {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : α) : Finset.filter (fun p => x = p.fst) (Multiset.toEnumFinset m) = Finset.map { toFun := Prod.mk x, inj' := (_ : Function.Injective (Prod.mk x)) } (Finset.range (Multiset.count x m))

@[simp]

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

@[simp]

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

@[simp]

theorem Multiset.map_univ_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) : Multiset.map (fun x => 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 => f x.fst) Finset.univ.val = Multiset.map f m

@[simp]

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

@[simp]

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

theorem Multiset.sum_eq_sum_coe {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) : Multiset.sum m = Finset.sum Finset.univ fun x => x.fst

theorem Multiset.prod_eq_prod_coe {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) : Multiset.prod m = Finset.prod Finset.univ fun x => x.fst

theorem Multiset.sum_eq_sum_toEnumFinset {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) : Multiset.sum m = Finset.sum (Multiset.toEnumFinset m) fun x => x.fst

theorem Multiset.prod_eq_prod_toEnumFinset {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) : Multiset.prod m = Finset.prod (Multiset.toEnumFinset m) fun x => x.fst

theorem Multiset.sum_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] (m : Multiset α) (f : α → ℕ → β) : (Finset.sum (Multiset.toEnumFinset m) fun x => f x.fst x.snd) = Finset.sum Finset.univ fun x => f x.fst ↑x.snd

theorem Multiset.prod_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [CommMonoid β] (m : Multiset α) (f : α → ℕ → β) : (Finset.prod (Multiset.toEnumFinset m) fun x => f x.fst x.snd) = Finset.prod Finset.univ fun x => f x.fst ↑x.snd