mathlib3 documentation

data.multiset.fintype

Multiset coercion to type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module defines a has_coe_to_sort instance for multisets and gives it a fintype instance. It also defines multiset.to_enum_finset, 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 decidable_eq α due to multiset.count.
multiset.to_enum_finset is a finset version of this.
multiset.coe_embedding is the embedding m ↪ α × ℕ, whose first component is the coercion and whose second component enumerates elements with multiplicity.
multiset.coe_equiv is the equivalence m ≃ m.to_enum_finset.

Tags #

multiset enumeration

@[nolint]

def multiset.to_type {α : Type u_1} [decidable_eq α] (m : multiset α) :

Type u_1

Auxiliary definition for the has_coe_to_sort instance. This prevents the has_coe m α instance from inadverently applying to other sigma types. One should not use this definition directly.

Equations

m.to_type = Σ (x : α), fin (multiset.count x m)

@[protected, instance]

def multiset.has_coe_to_sort {α : Type u_1} [decidable_eq α] :

has_coe_to_sort (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

multiset.has_coe_to_sort = {coe := multiset.to_type (λ (a b : α), _inst_1 a b)}

@[simp]

theorem multiset.coe_sort_eq {α : Type u_1} [decidable_eq α] {m : multiset α} :

m.to_type = ↥m

@[reducible]

def multiset.mk_to_type {α : Type u_1} [decidable_eq α] (m : multiset α) (x : α) (i : fin (multiset.count x m)) :

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

Equations

m.mk_to_type x i = ⟨x, i⟩

@[protected, instance]

def multiset.has_coe_to_sort.has_coe {α : Type u_1} [decidable_eq α] {m : multiset α} :

has_coe ↥m α

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

Equations

multiset.has_coe_to_sort.has_coe = {coe := λ (x : ↥m), x.fst}

@[simp]

theorem multiset.fst_coe_eq_coe {α : Type u_1} [decidable_eq α] {m : multiset α} {x : ↥m} :

@[simp]

theorem multiset.coe_eq {α : Type u_1} [decidable_eq α] {m : multiset α} {x y : ↥m} :

↑x = ↑y ↔ x.fst = y.fst

@[simp]

theorem multiset.coe_mk {α : Type u_1} [decidable_eq α] {m : multiset α} {x : α} {i : fin (multiset.count x m)} :

↑(m.mk_to_type x i) = x

@[simp]

theorem multiset.coe_mem {α : Type u_1} [decidable_eq α] {m : multiset α} {x : ↥m} :

@[protected, simp]

theorem multiset.forall_coe {α : Type u_1} [decidable_eq α] {m : multiset α} (p : ↥m → Prop) :

(∀ (x : ↥m), p x) ↔ ∀ (x : α) (i : fin (multiset.count x m)), p ⟨x, i⟩

@[protected, simp]

theorem multiset.exists_coe {α : Type u_1} [decidable_eq α] {m : multiset α} (p : ↥m → Prop) :

(∃ (x : ↥m), p x) ↔ ∃ (x : α) (i : fin (multiset.count x m)), p ⟨x, i⟩

@[protected, instance]

def set_of.fintype {α : Type u_1} [decidable_eq α] {m : multiset α} :

fintype ↥{p : α × ℕ | p.snd < multiset.count p.fst m}

Equations

set_of.fintype = fintype.of_finset (m.to_finset.bUnion (λ (x : α), finset.map {to_fun := prod.mk x, inj' := _} (finset.range (multiset.count x m)))) set_of.fintype._proof_1

def multiset.to_enum_finset {α : Type u_1} [decidable_eq α] (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.to_enum_finset = {p : α × ℕ | p.snd < multiset.count p.fst m}.to_finset

@[simp]

theorem multiset.mem_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) (p : α × ℕ) :

p ∈ m.to_enum_finset ↔ p.snd < multiset.count p.fst m

theorem multiset.mem_of_mem_to_enum_finset {α : Type u_1} [decidable_eq α] {m : multiset α} {p : α × ℕ} (h : p ∈ m.to_enum_finset) :

theorem multiset.to_enum_finset_mono {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} (h : m₁ ≤ m₂) :

m₁.to_enum_finset ⊆ m₂.to_enum_finset

@[simp]

theorem multiset.to_enum_finset_subset_iff {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} :

m₁.to_enum_finset ⊆ m₂.to_enum_finset ↔ m₁ ≤ m₂

@[simp]

theorem multiset.coe_embedding_apply {α : Type u_1} [decidable_eq α] (m : multiset α) (x : ↥m) :

⇑(m.coe_embedding) x = (↑x, ↑(x.snd))

def multiset.coe_embedding {α : Type u_1} [decidable_eq α] (m : multiset α) :

↥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 coe.

Equations

m.coe_embedding = {to_fun := λ (x : ↥m), (↑x, ↑(x.snd)), inj' := _}

@[simp]

theorem multiset.coe_equiv_symm_apply_fst {α : Type u_1} [decidable_eq α] (m : multiset α) (x : ↥(m.to_enum_finset)) :

(⇑(m.coe_equiv.symm) x).fst = x.val.fst

@[simp]

theorem multiset.coe_equiv_apply_coe {α : Type u_1} [decidable_eq α] (m : multiset α) (x : ↥m) :

↑(⇑(m.coe_equiv) x) = ⇑(m.coe_embedding) x

def multiset.coe_equiv {α : Type u_1} [decidable_eq α] (m : multiset α) :

↥m ≃ ↥(m.to_enum_finset)

Another way to coerce a multiset to a type is to go through m.to_enum_finset and coerce that finset to a type.

Equations

m.coe_equiv = {to_fun := λ (x : ↥m), ⟨⇑(m.coe_embedding) x, _⟩, inv_fun := λ (x : ↥(m.to_enum_finset)), ⟨x.val.fst, ⟨x.val.snd, _⟩⟩, left_inv := _, right_inv := _}

@[simp]

theorem multiset.coe_equiv_symm_apply_snd_val {α : Type u_1} [decidable_eq α] (m : multiset α) (x : ↥(m.to_enum_finset)) :

(⇑(m.coe_equiv.symm) x).snd.val = x.val.snd

@[simp]

theorem multiset.to_embedding_coe_equiv_trans {α : Type u_1} [decidable_eq α] (m : multiset α) :

m.coe_equiv.to_embedding.trans (function.embedding.subtype (λ (x : α × ℕ), x ∈ m.to_enum_finset)) = m.coe_embedding

@[protected, instance]

def multiset.fintype_coe {α : Type u_1} [decidable_eq α] {m : multiset α} :

Equations

multiset.fintype_coe = fintype.of_equiv ↥(m.to_enum_finset) m.coe_equiv.symm

theorem multiset.map_univ_coe_embedding {α : Type u_1} [decidable_eq α] (m : multiset α) :

finset.map m.coe_embedding finset.univ = m.to_enum_finset

theorem multiset.to_enum_finset_filter_eq {α : Type u_1} [decidable_eq α] (m : multiset α) (x : α) :

finset.filter (λ (p : α × ℕ), x = p.fst) m.to_enum_finset = finset.map {to_fun := prod.mk x, inj' := _} (finset.range (multiset.count x m))

@[simp]

theorem multiset.map_to_enum_finset_fst {α : Type u_1} [decidable_eq α] (m : multiset α) :

multiset.map prod.fst m.to_enum_finset.val = m

@[simp]

theorem multiset.image_to_enum_finset_fst {α : Type u_1} [decidable_eq α] (m : multiset α) :

finset.image prod.fst m.to_enum_finset = m.to_finset

@[simp]

theorem multiset.map_univ_coe {α : Type u_1} [decidable_eq α] (m : multiset α) :

multiset.map coe finset.univ.val = m

@[simp]

theorem multiset.map_univ {α : Type u_1} [decidable_eq α] {β : Type u_2} (m : multiset α) (f : α → β) :

multiset.map (λ (x : ↥m), f ↑x) finset.univ.val = multiset.map f m

@[simp]

theorem multiset.card_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :

m.to_enum_finset.card = ⇑multiset.card m

@[simp]

theorem multiset.card_coe {α : Type u_1} [decidable_eq α] (m : multiset α) :

fintype.card ↥m = ⇑multiset.card m

theorem multiset.prod_eq_prod_coe {α : Type u_1} [decidable_eq α] [comm_monoid α] (m : multiset α) :

m.prod = finset.univ.prod (λ (x : ↥m), ↑x)

theorem multiset.sum_eq_sum_coe {α : Type u_1} [decidable_eq α] [add_comm_monoid α] (m : multiset α) :

m.sum = finset.univ.sum (λ (x : ↥m), ↑x)

theorem multiset.sum_eq_sum_to_enum_finset {α : Type u_1} [decidable_eq α] [add_comm_monoid α] (m : multiset α) :

m.sum = m.to_enum_finset.sum (λ (x : α × ℕ), x.fst)

theorem multiset.prod_eq_prod_to_enum_finset {α : Type u_1} [decidable_eq α] [comm_monoid α] (m : multiset α) :

m.prod = m.to_enum_finset.prod (λ (x : α × ℕ), x.fst)

theorem multiset.prod_to_enum_finset {α : Type u_1} [decidable_eq α] {β : Type u_2} [comm_monoid β] (m : multiset α) (f : α → ℕ → β) :

m.to_enum_finset.prod (λ (x : α × ℕ), f x.fst x.snd) = finset.univ.prod (λ (x : ↥m), f ↑x ↑(x.snd))

theorem multiset.sum_to_enum_finset {α : Type u_1} [decidable_eq α] {β : Type u_2} [add_comm_monoid β] (m : multiset α) (f : α → ℕ → β) :

m.to_enum_finset.sum (λ (x : α × ℕ), f x.fst x.snd) = finset.univ.sum (λ (x : ↥m), f ↑x ↑(x.snd))