English
The product α × β, where α and β are generalized co-Heyting algebras, inherits a generalized co-Heyting algebra structure, defined componentwise by (x1,x2) \\ (y1,y2) = (x1 \\ y1, x2 \\ y2).
Русский
Произведение α × β, где α и β — обобщённые коейтинговые алгебры, наследует структуру обобщённой коейтинговой алгебры, задаваемую по компонентам: (x1,x2) \\ (y1,y2) = (x1 \\ y1, x2 \\ y2).
LaTeX
$$$ (\\alpha \\times \\beta) \\\\text{ carries a generalized co-Heyting algebra structure with } (x_1,x_2) \\\\setminus (y_1,y_2) = (x_1 \\\\setminus y_1, x_2 \\\\setminus y_2). $$$
Lean4
instance instGeneralizedCoheytingAlgebra [GeneralizedCoheytingAlgebra β] : GeneralizedCoheytingAlgebra (α × β) where
sdiff_le_iff _ _ _ := and_congr sdiff_le_iff sdiff_le_iff
