encode_ofNat — Mathlib

English

Encoding the nth element and then decoding returns the original element: encode (ofNat α n) = n.

Русский

Кодирование n-го элемента затем декодирование возвращает исходное число: encode (ofNat α n) = n.

LaTeX

$$$ \text{encode}(\text{ofNat } α n) = n $$$

Lean4

@[simp]
theorem encode_ofNat (n) : encode (ofNat α n) = n :=
  by
  obtain ⟨a, h, e⟩ := decode_inv (α := α) n
  rwa [ofNat_of_decode h]

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