instCompleteAtomicBooleanAlgebra — Mathlib

English

If α and β are CompleteAtomicBooleanAlgebras, then α × β is a CompleteAtomicBooleanAlgebra.

Русский

Если α и β — полные атомарные булевы алгебры, то их произведение α × β — полная атомарная булева алгебра.

LaTeX

$$$[CompleteAtomicBooleanAlgebra\; \alpha] \land [CompleteAtomicBooleanAlgebra\; \beta] \Rightarrow CompleteAtomicBooleanAlgebra(\alpha \times \beta).$$$

Lean4

instance instCompleteAtomicBooleanAlgebra [CompleteAtomicBooleanAlgebra α] [CompleteAtomicBooleanAlgebra β] :
    CompleteAtomicBooleanAlgebra (α × β) where
  __ := instBooleanAlgebra
  __ := instCompletelyDistribLattice

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