bit_lt_two_pow_succ_iff — Mathlib

English

For any boolean b and natural numbers x,n, the value bit_b(x) is less than 2^{n+1} if and only if x < 2^n.

Русский

Пусть b∈{0,1} и x,n∈ℕ. Значение битовой функции bit_b(x) меньше чем 2^{n+1} тогда и только тогда, когда x < 2^n.

LaTeX

$$$ \operatorname{bit}(b,x) < 2^{n+1} \iff x < 2^{n} $$$

Lean4

@[simp]
theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n := by cases b <;> simp <;> omega

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