instSProd — Mathlib

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

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