toBoolAlg_add — Mathlib

English

Let α be a Boolean ring. For all a,b ∈ α, the Boolean algebra image of a + b equals the symmetric difference of the images: toBoolAlg(a + b) = toBoolAlg(a) ∆ toBoolAlg(b).

Русский

Пусть α – булево кольцо. Для любых a,b ∈ α выполняется: toBoolAlg(a + b) = toBoolAlg(a) ∆ toBoolAlg(b).

LaTeX

$$$\operatorname{toBoolAlg}(a + b) = \operatorname{toBoolAlg}(a) \triangle \operatorname{toBoolAlg}(b)$$$

Lean4

@[simp]
theorem toBoolAlg_add (a b : α) : toBoolAlg (a + b) = toBoolAlg a ∆ toBoolAlg b :=
  (ofBoolAlg_symmDiff a b).symm

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