Encodable and Denumerable instances for Multiset

def encodeMultiset {α : Type u_1} [Encodable α] (s : Multiset α) : ℕ

Explicit encoding function for Multiset α

def decodeMultiset {α : Type u_1} [Encodable α] (n : ℕ) : Option (Multiset α)

Explicit decoding function for Multiset α

instance Multiset.encodable {α : Type u_1} [Encodable α] : Encodable (Multiset α)

If α is encodable, then so is Multiset α.

def Denumerable.lower : List ℕ → ℕ → List ℕ

Outputs the list of differences of the input list, that is lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]

def Denumerable.raise : List ℕ → ℕ → List ℕ

Outputs the list of partial sums of the input list, that is raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]

theorem Denumerable.lower_raise (l : List ℕ) (n : ℕ) : lower (raise l n) n = l

theorem Denumerable.raise_lower {l : List ℕ} {n : ℕ} : (n :: l).SortedLE → raise (lower l n) n = l

theorem Denumerable.isChain_raise (l : List ℕ) (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (raise l n)

theorem Denumerable.isChain_cons_raise (l : List ℕ) (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (n :: raise l n)

@[deprecated Denumerable.isChain_cons_raise (since := "2025-09-19")]

theorem Denumerable.raise_chain (l : List ℕ) (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (n :: raise l n)

Alias of Denumerable.isChain_cons_raise.

theorem Denumerable.raise_sorted (l : List ℕ) (n : ℕ) : (raise l n).SortedLE

raise l n is a non-decreasing sequence.

instance Denumerable.multiset {α : Type u_1} [Denumerable α] : Denumerable (Multiset α)

If α is denumerable, then so is Multiset α. Warning: this is not the same encoding as used in Multiset.encodable.