sup_sdiff_symmDiff — Mathlib

English

In a generalized Boolean algebra, the symmetric difference of a and b with respect to the join satisfies (a ∨ b) \\ a Δ b = a ∧ b.

Русский

В обобщённой булевой алгебре для элементов a и b выполняется: (a ∪ b) \\ a Δ b = a ∧ b.

LaTeX

$$$(a \\lor b) \\setminus a \\Delta b = a \\land b$$$

Lean4

@[simp]
theorem sup_sdiff_symmDiff : (a ⊔ b) \ a ∆ b = a ⊓ b :=
  sdiff_eq_symm inf_le_sup (by rw [symmDiff_eq_sup_sdiff_inf])

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