symmDiff_eq_top — Mathlib

English

For a,b in a Boolean algebra, a Δ b equals the top element if and only if a and b are complements.

Русский

Для элементов a и b булевой алгебры, a Δ b равно верхнему элементу тогда и только тогда, когда a и b — дополнения друг к другу.

LaTeX

$$$ a \triangle b = \top \\iff IsCompl(a,b) $$$

Lean4

@[simp]
theorem symmDiff_eq_top : a ∆ b = ⊤ ↔ IsCompl a b := by
  rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff, codisjoint_iff, and_comm]

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