instSProd

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.instSProd

English

The product s × t of Finsets s ⊆ α and t ⊆ β is the Finset of all pairs (a,b) with a ∈ s and b ∈ t.

Русский

Произведение Finset s и Finset t задаёт множество всех пар (a,b) с a ∈ s и b ∈ t.

LaTeX

$$$s \timesˢ t = \{ (a,b) : a \in s \wedge b \in t \}$$$

Lean4

instance instSProd : SProd (Finset α) (Finset β) (Finset (α × β)) where sprod := Finset.product

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru