compl_symmDiff_compl — Mathlib

English

The complement of the symmetric difference is invariant under complementing both arguments: (aᶜ Δ bᶜ) = a Δ b.

Русский

Комплемент симметрической разности сохраняется при взятии комплемента к обоим аргументам: aᶜ Δ bᶜ = a Δ b.

LaTeX

$$$ a^{\\complement} \\triangle b^{\\complement} = a \\triangle b $$$

Lean4

@[simp]
theorem compl_symmDiff_compl : aᶜ ∆ bᶜ = a ∆ b :=
  (sup_comm _ _).trans <| by simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

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