encodeSum — Mathlib

English

The encoding of the sum α ⊕ β into natural numbers is given by

Русский

Кодированиесложения α ⊕ β в натуральные числа задаётся следующим образом:

LaTeX

$$$ \mathrm{encodeSum}( \mathrm{Sum.inl}(a) ) = 2 \cdot \mathrm{encode}(a) \quad\text{and}\quad \mathrm{encodeSum}( \mathrm{Sum.inr}(b) ) = 2 \cdot \mathrm{encode}(b) + 1 $$$

Lean4

/-- Explicit encoding function for the sum of two encodable types. -/
def encodeSum : α ⊕ β → ℕ
  | Sum.inl a => 2 * encode a
  | Sum.inr b => 2 * encode b + 1

Похожие утверждения