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.

@[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 α} : s.toList.isEmpty = true ↔ s = 0

@[simp]

theorem Multiset.toList_zero {α : Type u_1} : toList 0 = []

@[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 : α) : {a}.toList = [a]

@[simp]

theorem Multiset.length_toList {α : Type u_1} (s : Multiset α) : s.toList.length = s.card

Induction principles

@[irreducible]

def Multiset.strongInductionOn {α : Type u_1} {p : Multiset α → Sort u_2} (s : Multiset α) (ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s) : p s

The strong induction principle for multisets.

theorem Multiset.strongInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_2} (s : Multiset α) (H : (s : Multiset α) → ((t : Multiset α) → t < s → p 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 ≤ s → p t) → p (a ::ₘ s)) : p s

@[irreducible]

def Multiset.strongDownwardInduction {α : Type u_1} {p : Multiset α → Sort u_2} {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α) : s.card ≤ n → p 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.

theorem Multiset.strongDownwardInduction_eq {α : Type u_1} {p : Multiset α → Sort u_2} {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p 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_2} {n : ℕ} (s : Multiset α) : ((t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) → s.card ≤ n → p s

Analogue of strongDownwardInduction with order of arguments swapped.

theorem Multiset.strongDownwardInductionOn_eq {α : Type u_1} {p : Multiset α → Sort u_2} (s : Multiset α) {n : ℕ} (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p 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.

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.

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)

theorem Multiset.choose_eq_iff {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Multiset α) (hp : ∃! a : α, a ∈ l ∧ p a) {a : α} : choose p l hp = a ↔ a ∈ l ∧ p a

def Multiset.subsingletonEquiv (α : Type u_1) [Subsingleton α] : List α ≃ Multiset α

The equivalence between lists and multisets of a subsingleton type.

@[simp]

theorem Multiset.coe_subsingletonEquiv {α : Type u_1} [Subsingleton α] : ⇑(subsingletonEquiv α) = ofList