bit — Mathlib

English

bit b n appends the bit b to the least-significant end of the binary representation of n.

Русский

bit b n добавляет последние цифры двоичного представления числа n: если b=true, добавляется 1, иначе 0.

LaTeX

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

Lean4

/-- `bit b` appends the digit `b` to the little end of the binary representation of
its natural number input. -/
def bit (b : Bool) (n : Nat) : Nat :=
  cond b (2 * n + 1) (2 * n)

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