encodingNatBool — Mathlib

English

A binary encoding of natural numbers into booleans is given by encodingNatBool.

Русский

Дано бинарное кодирование натуральных чисел в булевы значения: encodingNatBool.

LaTeX

$$$ \text{encodingNatBool} : Encoding\,\mathbb{N} $$$

Lean4

/-- A binary encoding of ℕ in bool. -/
def encodingNatBool : Encoding ℕ where
  Γ := Bool
  encode := encodeNat
  decode n := some (decodeNat n)
  decode_encode n := congr_arg _ (decode_encodeNat n)

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