English
The product of two Boolean algebras α × β carries a Boolean algebra structure, obtained from the componentwise operations and compatible with sup, inf, and sdiff.
Русский
Произведение двух булевых алгебр α × β наследует структуру булевой алгебры по покомпонентным операциям, совместимым с sup, inf и sdiff.
LaTeX
$$$\text{BooleanAlgebra}(\alpha \times \beta)$ with componentwise operations and the specified equalities$$
Lean4
instance instBooleanAlgebra [BooleanAlgebra α] [BooleanAlgebra β] : BooleanAlgebra (α × β)
where
__ := instDistribLattice α β
__ := instHeytingAlgebra
himp_eq x y := by ext <;> simp [himp_eq]
sdiff_eq x y := by ext <;> simp [sdiff_eq]
inf_compl_le_bot x := by constructor <;> simp
top_le_sup_compl x := by constructor <;> simp
