lor_bit — Mathlib

English

The bitwise OR distributes over the bit construction: bit a m ||| bit b n = bit (a ∨ b) (m ||| n).

Русский

Побитовое OR распространяется через конструирование бит: bit a m ||| bit b n = bit (a ∨ b) (m ||| n).

LaTeX

$$$$ \\text{bitarith: } bit\\ a\\ m \\lor\\lor\\ bit\\ b\\ n = bit (a \\lor b) (m \\lor\\lor n) $$$$

Lean4

@[simp]
theorem lor_bit : ∀ a m b n, bit a m ||| bit b n = bit (a || b) (m ||| n) :=
  bitwise_bit

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