bit — Mathlib

English

bit(b) appends the bit b to the binary representation of its integer input: true adds 1, false adds 0 at the least significant bit.

Русский

bit(b) дописывает бит b к двоичному представлению числа: true добавляет 1, false — 0 в младший разряд.

LaTeX

$$$\\mathrm{bit}(b)(x) = \\begin{cases} 2x+1, & b = \\text{true} \\\\ 2x, & b = \\text{false} \\end{cases}$$$

Lean4

/-- `bit b` appends the digit `b` to the binary representation of
  its integer input. -/
def bit (b : Bool) : ℤ → ℤ :=
  cond b (2 * · + 1) (2 * ·)

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