testBit_lor

Mathlib.Data.Nat.Bitwise

URI: https://scilib.ai/kg/mathlib#Nat.testBit_lor

English

testBit distributes over bitwise OR: testBit (m ||| n) k = (testBit m k) ∨ (testBit n k).

Русский

testBit распределяется через побитовое OR: testBit (m ||| n) k = testBit m k ∨ testBit n k.

LaTeX

$$$$ \\text{testBit}(m\\,|||\\,n)\\,k = \\text{testBit}(m)\\,k \\lor \\text{testBit}(n)\\,k $$$$

Lean4

theorem testBit_lor : ∀ m n k, testBit (m ||| n) k = (testBit m k || testBit n k) :=
  testBit_bitwise rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru