toBoolAlg_mul — Mathlib

English

The image under toBoolAlg of a product equals the meet of images: toBoolAlg(a · b) = toBoolAlg(a) ∧ toBoolAlg(b).

Русский

Образ произведения через toBoolAlg равен пределу образов: toBoolAlg(a · b) = toBoolAlg(a) ∧ toBoolAlg(b).

LaTeX

$$$\mathrm{toBoolAlg}(a \cdot b) = \mathrm{toBoolAlg}(a) \wedge \mathrm{toBoolAlg}(b)$$$

Lean4

@[simp]
theorem toBoolAlg_mul (a b : α) : toBoolAlg (a * b) = toBoolAlg a ⊓ toBoolAlg b :=
  rfl

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