English
There is a canonical SProd structure on LowerSet α and LowerSet β with sprod given by LowerSet.prod.
Русский
Существует каноническая структура SProd на LowerSet α и LowerSet β, определяемая через prod.
LaTeX
$$$\text{instance } \text{instSProd} : SProd (\text{LowerSet } α) (\text{LowerSet } β) (\text{LowerSet } (α \times β)) \text{ where } sprod := \text{LowerSet.prod}$$$
Lean4
instance instSProd : SProd (LowerSet α) (LowerSet β) (LowerSet (α × β)) where sprod := LowerSet.prod