ofBoolAlg_sup — Mathlib

English

The map ofBoolAlg sends a ⊔ b to the sum of images plus their product: ofBoolAlg(a ⊔ b) = ofBoolAlg(a) + ofBoolAlg(b) + ofBoolAlg(a)·ofBoolAlg(b).

Русский

Отображение ofBoolAlg переводит a ⊔ b в сумму образов плюс их произведение: ofBoolAlg(a ⊔ b) = ofBoolAlg(a) + ofBoolAlg(b) + ofBoolAlg(a)·ofBoolAlg(b).

LaTeX

$$$\mathrm{ofBoolAlg}(a \lor b) = \mathrm{ofBoolAlg}(a) + \mathrm{ofBoolAlg}(b) + \mathrm{ofBoolAlg}(a)\cdot\mathrm{ofBoolAlg}(b)$$$

Lean4

@[simp]
theorem ofBoolAlg_sup (a b : AsBoolAlg α) : ofBoolAlg (a ⊔ b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b :=
  rfl

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