toBoolAlg_add_add_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toBoolAlg_add_add_mul (a b : α) : toBoolAlg (a + b + a * b) = toBoolAlg a ⊔ toBoolAlg b :=
  rfl

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