unaryFinEncodingNat — Mathlib

English

A unary FinEncoding of ℕ exists, defined using unary encoding.

Русский

Существует унарное FinEncoding ℕ, задаваемое через унарное кодирование.

LaTeX

$$$ \text{unaryFinEncodingNat} : FinEncoding\,\mathbb{N} $$$

Lean4

/-- A unary fin_encoding of ℕ. -/
def unaryFinEncodingNat : FinEncoding ℕ where
  Γ := Bool
  encode := unaryEncodeNat
  decode n := some (unaryDecodeNat n)
  decode_encode n := congr_arg _ (unary_decode_encode_nat n)
  ΓFin := Bool.fintype

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