English
If α and β are generalized Boolean algebras, then their Cartesian product α × β is a generalized Boolean algebra, defined componentwise.
Русский
Если α и β — обобщённые буловы алгебры, то их декартово произведение α × β является обобщённой булевой алгеброй, операции определяются по компонентам.
LaTeX
$$$\\alpha \\text{ и } \\beta \\text{ — обобщённые булевые алгебры } \\Rightarrow (\\alpha \\times \\beta) \\text{ — обобщённая булева алгебра, с оперaциями по компонентам.}$$$
Lean4
instance instGeneralizedBooleanAlgebra [GeneralizedBooleanAlgebra β] : GeneralizedBooleanAlgebra (α × β)
where
sup_inf_sdiff _ _ := Prod.ext (sup_inf_sdiff _ _) (sup_inf_sdiff _ _)
inf_inf_sdiff _
_ :=
Prod.ext (inf_inf_sdiff _ _)
(inf_inf_sdiff _ _)
-- Porting note: Once `pi_instance` has been ported, this is just `by pi_instance`.
