trPosNum_natEnd — Mathlib

English

For every PosNum, any element of its translation trPosNum has natEnd x = false, i.e., the encoding ends with a non-terminating bit pattern.

Русский

Для каждого PosNum каждое элемент из trPosNum имеет natEnd x = false: кодировка завершается не размерной концовкой.

LaTeX

$$$\\forall n\\in \\text{PosNum},\\; \\forall x\\in \\operatorname{trPosNum} (n),\\; \\operatorname{natEnd}(x)=\\text{false}$$$

Lean4

theorem trPosNum_natEnd : ∀ (n), ∀ x ∈ trPosNum n, natEnd x = false
  | PosNum.one, _, List.Mem.head _ => rfl
  | PosNum.bit0 _, _, List.Mem.head _ => rfl
  | PosNum.bit0 n, _, List.Mem.tail _ h => trPosNum_natEnd n _ h
  | PosNum.bit1 _, _, List.Mem.head _ => rfl
  | PosNum.bit1 n, _, List.Mem.tail _ h => trPosNum_natEnd n _ h

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