testBit_lnot — Mathlib

English

For all integers n and natural k, testBit (lnot n) k equals not (testBit n k).

Русский

Для любого целого n и натурального k: k-й бит lnot n равен неравному к этому биту n.

LaTeX

$$$$\forall n\in\mathbb{Z},\; \forall k\in\mathbb{N},\; \mathrm{testBit}(\mathrm{lnot}\, n)\ k = \lnot(\mathrm{testBit}\, n\ k).$$$$

Lean4

@[simp]
theorem testBit_lnot : ∀ n k, testBit (lnot n) k = not (testBit n k)
  | (n : ℕ), k => by simp [lnot, testBit]
  | -[n+1], k => by simp [lnot, testBit]

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