Encodable and Denumerable instances for Multiset

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

Explicit encoding function for Multiset α

Equations

• encodeMultiset s = Encodable.encode (Multiset.sort enle✝ s)

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

Explicit decoding function for Multiset α

Equations

• decodeMultiset n = Multiset.ofList <$> Encodable.decode n

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

If α is encodable, then so is Multiset α.

Equations

• Multiset.encodable = { encode := encodeMultiset, decode := decodeMultiset, encodek := ⋯ }

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

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

Equations

• Denumerable.lower [] x✝ = []
• Denumerable.lower (m :: l) x✝ = (m - x✝) :: Denumerable.lower l m

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₂, ...]

Equations

• Denumerable.raise [] x✝ = []
• Denumerable.raise (m :: l) x✝ = (m + x✝) :: Denumerable.raise l (m + x✝)

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

theorem Denumerable.raise_lower {l : List ℕ} {n : ℕ} : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (n :: l) → 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 : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (raise l n)

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.

Equations

• One or more equations did not get rendered due to their size.