top_symmDiff'

Mathlib.Order.SymmDiff

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

English

Symmetric difference with the top element on the left also yields the negation: ⊤ Δ a = ¬a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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