compl_bihimp

Mathlib.Order.SymmDiff

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

English

In a Boolean algebra, the complement of the biconditional equals the symmetric difference: (a ⇔ b)ᶜ = a Δ b.

Русский

В булевой алгебре комплемент биимпликации равен симметрической разности: (a ⇔ b)ᶜ = a Δ b.

LaTeX

$$$ (a \Leftrightarrow b)^{\\complement} = a \\triangle b $$$

Lean4

@[simp]
theorem compl_bihimp : (a ⇔ b)ᶜ = a ∆ b :=
  @compl_symmDiff αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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