coe_xor_iff

Mathlib.Data.Bool.Basic

URI: https://scilib.ai/kg/mathlib#Bool.coe_xor_iff

English

For booleans a,b, xor a b = true iff exactly one of a,b is true, i.e., equivalent to Xor'(a = true) (b = true).

Русский

Для булевых значений a,b, a ⊕ b = true тогда и только тогда, когда ровно одно из a,b истинно.

LaTeX

$$$$ (a \oplus b) = \mathrm{true} \;\iff\; a \neq b $$$$

Lean4

theorem coe_xor_iff (a b : Bool) : xor a b ↔ Xor' (a = true) (b = true) := by grind

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

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

Разделы

Аффилиация

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