decode_encodePosNum — Mathlib

English

Decoding after encoding returns the original PosNum: decodePosNum (encodePosNum n) = n.

Русский

Декодирование после кодирования возвращает исходное PosNum: decodePosNum (encodePosNum n) = n.

LaTeX

$$$ decodePosNum (encodePosNum n) = n $$$

Lean4

@[simp]
theorem decode_encodePosNum (n) : decodePosNum (encodePosNum n) = n := by
  induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm

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