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.

Equations

• Multiset.ToType m = ((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 with different values of i.

Equations

• instCoeSortMultisetType = { coe := Multiset.ToType }

@[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.

Equations

• Multiset.mkToType m x i = { fst := x, snd := i }

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.

Equations

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

@[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 : Multiset.ToType m), p x) ↔ ∃ (x : α) (i : Fin (Multiset.count x m)), p { fst := x, snd := i }

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

Equations

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

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

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

@[simp]

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

theorem Multiset.mem_of_mem_toEnumFinset {α : Type u_1} [DecidableEq α] {m : Multiset α} {p : α × ℕ} (h : p ∈ Multiset.toEnumFinset m) : p.1 ∈ 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 (↑).

Equations

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

@[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).1

@[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).2

@[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.

Equations

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

@[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)

Equations

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

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.1) (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 : Multiset.ToType m) => 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 : Multiset.ToType m) => f x.fst) Finset.univ.val = Multiset.map f m

@[simp]

theorem Multiset.card_toEnumFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) : (Multiset.toEnumFinset m).card = 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 : Multiset.ToType m) => x.fst

theorem Multiset.prod_eq_prod_coe {α : Type u_1} [DecidableEq α] [CommMonoid α] (m : Multiset α) : Multiset.prod m = Finset.prod Finset.univ fun (x : Multiset.ToType m) => 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.1

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

theorem Multiset.sum_toEnumFinset {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] (m : Multiset α) (f : α → ℕ → β) : (Finset.sum (Multiset.toEnumFinset m) fun (x : α × ℕ) => f x.1 x.2) = Finset.sum Finset.univ fun (x : Multiset.ToType m) => 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.1 x.2) = Finset.prod Finset.univ fun (x : Multiset.ToType m) => f x.fst ↑x.snd