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 Multiset.instCoeSortType {α : 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

• Multiset.instCoeSortType = { coe := Multiset.ToType }

@[reducible, match_pattern]

def Multiset.mkToType {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : α) (i : Fin (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 Multiset.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

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

theorem Multiset.coe_mk {α : Type u_1} [DecidableEq α] {m : Multiset α} {x : α} {i : Fin (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 (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 (count x m)), p ⟨x, i⟩

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

Equations

• Multiset.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 < 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 (count a m)

@[simp]

theorem Multiset.map_toEnumFinset_fst {α : Type u_1} [DecidableEq α] (m : 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) : map Prod.fst s.val ≤ m

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

@[simp]

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

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.coeEmbedding_apply {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) : m.coeEmbedding x = (x.fst, ↑x.snd)

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.coeEquiv_apply_coe {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : m.ToType) : ↑(m.coeEquiv x) = m.coeEmbedding x

@[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_symm_apply_snd_val {α : Type u_1} [DecidableEq α] (m : Multiset α) (x : { x : α × ℕ // x ∈ m.toEnumFinset }) : ↑(m.coeEquiv.symm x).snd = (↑x).2

@[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 α) : map (fun (x : m.ToType) => x.fst) Finset.univ.val = m

@[simp]

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

@[simp]

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

@[simp]

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

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_coe {α : Type u_1} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) : m.sum = ∑ x : m.ToType, x.fst

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

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

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

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

def Multiset.cast {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s = t) : s.ToType ≃ t.ToType

If s = t then there's an equivalence between the appropriate types.

Equations

• Multiset.cast h = { toFun := fun (x : s.ToType) => ⟨x.fst, Fin.cast ⋯ x.snd⟩, invFun := fun (x : t.ToType) => ⟨x.fst, Fin.cast ⋯ x.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Multiset.cast_apply_fst {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s = t) (x : s.ToType) : ((cast h) x).fst = x.fst

@[simp]

theorem Multiset.cast_symm_apply_snd {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s = t) (x : t.ToType) : ((cast h).symm x).snd = Fin.cast ⋯ x.snd

@[simp]

theorem Multiset.cast_apply_snd {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s = t) (x : s.ToType) : ((cast h) x).snd = Fin.cast ⋯ x.snd

@[simp]

theorem Multiset.cast_symm_apply_fst {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s = t) (x : t.ToType) : ((cast h).symm x).fst = x.fst

instance Multiset.instIsEmptyToTypeOfNat {α : Type u_1} [DecidableEq α] : IsEmpty (ToType 0)

instance Multiset.instIsEmptyToTypeEmptyCollection {α : Type u_1} [DecidableEq α] : IsEmpty ∅.ToType

def Multiset.consEquiv {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} : (v ::ₘ m).ToType ≃ Option m.ToType

v ::ₘ m is equivalent to Option m by mapping one v to none and everything else to m.

Equations

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

@[simp]

theorem Multiset.consEquiv_symm_none {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} : consEquiv.symm none = ⟨v, ⟨count v m, ⋯⟩⟩

@[simp]

theorem Multiset.consEquiv_symm_some {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} {x : m.ToType} : consEquiv.symm (some x) = ⟨x.fst, Fin.castLE ⋯ x.snd⟩

theorem Multiset.coe_consEquiv_of_ne {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType) (hx : x.fst ≠ v) : consEquiv x = some ⟨x.fst, Fin.cast ⋯ x.snd⟩

theorem Multiset.coe_consEquiv_of_eq_of_eq {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType) (hx : x.fst = v) (hx2 : ↑x.snd = count v m) : consEquiv x = none

theorem Multiset.coe_consEquiv_of_eq_of_lt {α : Type u_1} [DecidableEq α] {m : Multiset α} {v : α} (x : (v ::ₘ m).ToType) (hx : x.fst = v) (hx2 : ↑x.snd < count v m) : consEquiv x = some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

def Multiset.mapEquiv_aux {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Multiset α) (f : α → β) : Squash { v : m.ToType ≃ (map f m).ToType // ∀ (a : m.ToType), (v a).fst = f a.fst }

There is some equivalence between m and m.map f which respects f.

Equations

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

noncomputable def Multiset.mapEquiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → β) : s.ToType ≃ (map f s).ToType

One of the possible equivalences from Multiset.mapEquiv_aux, selected using choice.

Equations

• s.mapEquiv f = ↑(Quot.out (s.mapEquiv_aux f))

@[simp]

theorem Multiset.mapEquiv_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → β) (v : s.ToType) : ((s.mapEquiv f) v).fst = f v.fst