bit_to_nat — Mathlib

English

The binary bit construction for a Bool and a positive natural matches the standard Nat.bit construction.

Русский

Бинарная конструкция бита и позиции в PosNum совпадает с обычной битовой записью Nat.bit.

LaTeX

$$$\\forall b \\in \\{\\text{false, true}\\}, \\forall n \\in \\text{PosNum},\\; (\\text{bit } b\\, n : \\mathbb{N}) = \\operatorname{Nat.bit} b n$$$

Lean4

@[simp, norm_cast]
theorem bit_to_nat (b n) : (bit b n : ℕ) = Nat.bit b n := by cases b <;> simp [bit, two_mul]

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