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 #

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
@[protected, instance]

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
@[simp]
theorem multiset.coe_sort_eq {α : Type u_1} [decidable_eq α] {m : multiset α} :
@[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
@[protected, instance]

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

Equations
@[simp]
theorem multiset.fst_coe_eq_coe {α : Type u_1} [decidable_eq α] {m : multiset α} {x : m} :
x.fst = x
@[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} :
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 α} :
Equations
def multiset.to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) :

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
@[simp]
theorem multiset.mem_to_enum_finset {α : Type u_1} [decidable_eq α] (m : multiset α) (p : α × ) :
theorem multiset.mem_of_mem_to_enum_finset {α : Type u_1} [decidable_eq α] {m : multiset α} {p : α × } (h : p m.to_enum_finset) :
p.fst m
theorem multiset.to_enum_finset_mono {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} (h : m₁ m₂) :
@[simp]
theorem multiset.to_enum_finset_subset_iff {α : Type u_1} [decidable_eq α] {m₁ m₂ : multiset α} :
@[simp]
theorem multiset.coe_embedding_apply {α : Type u_1} [decidable_eq α] (m : multiset α) (x : m) :
def multiset.coe_embedding {α : Type u_1} [decidable_eq α] (m : multiset α) :

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
@[simp]
theorem multiset.coe_equiv_symm_apply_fst {α : Type u_1} [decidable_eq α] (m : multiset α) (x : (m.to_enum_finset)) :
@[simp]
theorem multiset.coe_equiv_apply_coe {α : Type u_1} [decidable_eq α] (m : multiset α) (x : m) :
def multiset.coe_equiv {α : Type u_1} [decidable_eq α] (m : multiset α) :

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
@[simp]
@[protected, instance]
def multiset.fintype_coe {α : Type u_1} [decidable_eq α] {m : multiset α} :
Equations
theorem multiset.to_enum_finset_filter_eq {α : Type u_1} [decidable_eq α] (m : multiset α) (x : α) :
@[simp]
@[simp]
theorem multiset.map_univ {α : Type u_1} [decidable_eq α] {β : Type u_2} (m : multiset α) (f : α β) :
@[simp]
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))