bit_val

Mathlib.Data.Nat.BinaryRec

URI: https://scilib.ai/kg/mathlib#Nat.bit_val

English

The bit function satisfies bit b n = 2·n + toNat(b).

Русский

Функция bit удовлетворяет bit b n = 2·n + toNat(b).

LaTeX

$$$\forall (b:Bool) (n:\mathbb{N}),\; \text{bit}\; b\; n = 2 \cdot n + b^{\text{toNat}}$$$

Lean4

theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by cases b <;> rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru