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]