symmDiff_top'

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#symmDiff_top'

English

In a Coheyting algebra, a Δ ⊤ = ¬a; symmetric difference with the top element yields negation.

Русский

В коейитингевой алгебре a Δ ⊤ = ¬a; симметрическая разность с верхним элементом даёт отрицание.

LaTeX

$$$a \Delta \top = \neg a$$$

Lean4

@[simp]
theorem symmDiff_top' : a ∆ ⊤ = ￢a := by simp [symmDiff]

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

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

Разделы

Аффилиация

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