Documentation

Mathlib.Data.Multiset.Basic

Basic results on multisets #

Multiset.toList #

noncomputable def Multiset.toList {α : Type u_1} (s : Multiset α) :
List α

Produces a list of the elements in the multiset using choice.

Equations
@[simp]
theorem Multiset.coe_toList {α : Type u_1} (s : Multiset α) :
s.toList = s
@[simp]
theorem Multiset.toList_eq_nil {α : Type u_1} {s : Multiset α} :
s.toList = [] s = 0
theorem Multiset.empty_toList {α : Type u_1} {s : Multiset α} :
@[simp]
theorem Multiset.toList_zero {α : Type u_1} :
@[simp]
theorem Multiset.mem_toList {α : Type u_1} {a : α} {s : Multiset α} :
a s.toList a s
@[simp]
theorem Multiset.toList_eq_singleton_iff {α : Type u_1} {a : α} {m : Multiset α} :
m.toList = [a] m = {a}
@[simp]
theorem Multiset.toList_singleton {α : Type u_1} (a : α) :
@[simp]
theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) :

Induction principles #

@[irreducible]
def Multiset.strongInductionOn {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) (ih : (s : Multiset α) → ((t : Multiset α) → t < sp t)p s) :
p s

The strong induction principle for multisets.

Equations
theorem Multiset.strongInductionOn_eq {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) (H : (s : Multiset α) → ((t : Multiset α) → t < sp t)p s) :
s.strongInductionOn H = H s fun (t : Multiset α) (_h : t < s) => t.strongInductionOn H
theorem Multiset.case_strongInductionOn {α : Type u_1} {p : Multiset αProp} (s : Multiset α) (h₀ : p 0) (h₁ : ∀ (a : α) (s : Multiset α), (∀ (t : Multiset α), t sp t)p (a ::ₘ s)) :
p s
@[irreducible]
def Multiset.strongDownwardInduction {α : Type u_1} {p : Multiset αSort u_3} {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) (s : Multiset α) :
s.card np s

Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all multisets s of cardinality less than n, starting from multisets of card n and iterating. This can be used either to define data, or to prove properties.

Equations
theorem Multiset.strongDownwardInduction_eq {α : Type u_1} {p : Multiset αSort u_3} {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) (s : Multiset α) :
strongDownwardInduction H s = H s fun {t₂ : Multiset α} (ht : t₂.card n) (_hst : s < t₂) => strongDownwardInduction H t₂ ht
def Multiset.strongDownwardInductionOn {α : Type u_1} {p : Multiset αSort u_3} {n : } (s : Multiset α) :
((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁)s.card np s

Analogue of strongDownwardInduction with order of arguments swapped.

Equations
theorem Multiset.strongDownwardInductionOn_eq {α : Type u_1} {p : Multiset αSort u_3} (s : Multiset α) {n : } (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card nt₁ < t₂p t₂)t₁.card np t₁) :
(fun (a : s.card n) => s.strongDownwardInductionOn H a) = H s fun {t : Multiset α} (ht : t.card n) (_h : s < t) => t.strongDownwardInductionOn H ht
def Multiset.chooseX {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (_hp : ∃! a : α, a l p a) :
{ a : α // a l p a }

Given a proof hp that there exists a unique a ∈ l such that p a, chooseX p l hp returns that a together with proofs of a ∈ l and p a.

Equations
  • One or more equations did not get rendered due to their size.
def Multiset.choose {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
α

Given a proof hp that there exists a unique a ∈ l such that p a, choose p l hp returns that a.

Equations
theorem Multiset.choose_spec {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
choose p l hp l p (choose p l hp)
theorem Multiset.choose_mem {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
choose p l hp l
theorem Multiset.choose_property {α : Type u_1} (p : αProp) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a l p a) :
p (choose p l hp)

The equivalence between lists and multisets of a subsingleton type.

Equations
@[deprecated "Deprecated without replacement." (since := "2025-02-07")]
theorem Multiset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Multiset α} (hx : x s) :