bits_append_bit — Mathlib

English

For any n and b, bits(bit b n) = b :: n.bits, provided that if n = 0 then b = true.

Русский

Для любого n и b: bits(bit b n) = b :: n.bits при условии, что если n = 0, то b = true.

LaTeX

$$$$ \text{bits}(\text{bit}(b,n)) = b \;::\; \text{bits}(n) \quad\text{(при условии } n=0 \Rightarrow b=\text{true}). $$$$

Lean4

@[simp]
theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) : (bit b n).bits = b :: n.bits :=
  by
  rw [Nat.bits, Nat.bits, binaryRec_eq]
  simpa

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