compl_symmDiff_self

Mathlib.Order.SymmDiff

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

English

The symmetric difference of a with its complement is the top element: aᶜ Δ a = ⊤.

Русский

Симметрическая разность элемента и его дополнения равна верхнему элементу: aᶜ Δ a = ⊤.

LaTeX

$$$ a^{\\complement} \\triangle a = \\top $$$

Lean4

@[simp]
theorem compl_symmDiff_self : aᶜ ∆ a = ⊤ :=
  hnot_symmDiff_self _

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

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

Разделы

Аффилиация

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