hnot_symmDiff_self — Mathlib

English

In a Coheyting algebra, (¬a) Δ a = ⊤; the negation and a are complement with respect to top.

Русский

В коейтинговой алгебре (¬a) Δ a = ⊤; отрицание и a образуют дополнение к верхнему элементу.

LaTeX

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

Lean4

@[simp]
theorem hnot_symmDiff_self : (￢a) ∆ a = ⊤ :=
  by
  rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
  exact Codisjoint.top_le codisjoint_hnot_left

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