instSProd — Mathlib

English

The product structure SProd on (Set α) and (Set β) is instantiated by Set.prod.

Русский

Структура произведения SProd над (Set α) и (Set β) задаётся через Set.prod.

LaTeX

$$$$\\text{instSProd: } SProd(\\mathrm{Set}\\,\\alpha)(\\mathrm{Set}\\,\\beta)(\\mathrm{Set}(\\alpha\\times\\beta))\\text{ with } sprod := \\mathrm{Set.prod}.$$$$

Lean4

@[default_instance]
instance instSProd : SProd (Set α) (Set β) (Set (α × β)) where sprod := Set.prod

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