unary_decode_encode_nat — Mathlib

English

Encoding followed by decoding yields the original number: unaryDecodeNat (unaryEncodeNat n) = n.

Русский

Кодирование с последующим декодированием возвращает исходное число: unaryDecodeNat (unaryEncodeNat n) = n.

LaTeX

$$$ \forall n, \ \mathrm{unaryDecodeNat}(\mathrm{unaryEncodeNat}(n)) = n $$$

Lean4

@[simp]
theorem unary_decode_encode_nat : ∀ n, unaryDecodeNat (unaryEncodeNat n) = n := fun n =>
  Nat.rec rfl (fun (_m : ℕ) hm => (congr_arg Nat.succ hm.symm).symm) n

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