compl_symmDiff — Mathlib

English

Let a and b be elements of a Boolean algebra. Then the complement of their symmetric difference equals their biconditional: (a Δ b)^c = a ⇔ b.

Русский

Пусть a и b — элементы булевой алгебры. Тогда комплемент симметрической разности a и b равен их биэквиваленции: (a Δ b)^c = a ⇔ b.

LaTeX

$$$ (a \\triangle b)^{\\complement} = a \\Leftrightarrow b $$$

Lean4

@[simp]
theorem compl_symmDiff : (a ∆ b)ᶜ = a ⇔ b := by simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]

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