not_xor

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#not_xor

English

For propositions P and Q, not (P ⊕ Q) is equivalent to (P ↔ Q).

Русский

Для высказываний P и Q не P⊕Q эквивалентно P ⇔ Q.

LaTeX

$$$\\\\neg(Xor'(P,Q))\\\\leftrightarrow(P\\\\leftrightarrow Q)$$$

Lean4

@[simp]
theorem not_xor (P Q : Prop) : ¬Xor' P Q ↔ (P ↔ Q) := by
  simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]

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

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

Разделы

Аффилиация

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