zero_of_testBit_eq_false — Mathlib

English

If a natural number n has every testBit equal to false, then n is zero.

Русский

Если для натурального числа n выполняется, что для всех i тестовый бит testBit(n,i) равен false, то n = 0.

LaTeX

$$$\forall i:\ testBit(n,i)=\text{false} \Rightarrow n=0$$$

Lean4

theorem zero_of_testBit_eq_false {n : ℕ} (h : ∀ i, testBit n i = false) : n = 0 :=
  by
  induction n using Nat.binaryRec with
  | zero => rfl
  | bit b n hn => ?_
  have : b = false := by simpa using h 0
  rw [this, bit_false, hn fun i => by rw [← h (i + 1), testBit_bit_succ]]

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