lor_bit

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.lor_bit

English

For booleans a,b and integers m,n, lor (bit a m) (bit b n) equals bit (a ∨ b) (lor m n).

Русский

Для булевых a,b и целых m,n: lor (bit a m) (bit b n) = bit (a ∨ b) (lor m n).

LaTeX

$$$$ \operatorname{lor\_{bit}}(a,m,b,n) = \operatorname{bit}(a \lor b)(\operatorname{lor} m n). $$$$

Lean4

@[simp]
theorem lor_bit (a m b n) : lor (bit a m) (bit b n) = bit (a || b) (lor m n) := by rw [← bitwise_or, bitwise_bit]

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

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

Разделы

Аффилиация

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