testBit_lor — Mathlib

English

For all integers m, n and natural k, testBit (lor m n) k equals (testBit m k) or (testBit n k).

Русский

Пусть m, n — целые, k — натуральное. Тогда k-й бит числа lor m n равен логическому OR k-й биту m и k-й биту n.

LaTeX

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

Lean4

@[simp]
theorem testBit_lor (m n k) : testBit (lor m n) k = (testBit m k || testBit n k) := by
  rw [← bitwise_or, testBit_bitwise]

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