instFintypeProd

Mathlib.Data.Fintype.Prod

URI: https://scilib.ai/kg/mathlib#instFintypeProd

English

The Cartesian product α × β is finite when α and β are finite.

Русский

Декартово произведение α × β конечно, если α и β конечны.

LaTeX

$$$(\\alpha \\times \\beta)$ is finite, i.e., $Fintype(\\alpha \\times \\beta)$.$$

Lean4

instance instFintypeProd (α β : Type*) [Fintype α] [Fintype β] : Fintype (α × β) :=
  ⟨univ ×ˢ univ, fun ⟨a, b⟩ => by simp⟩

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

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

Разделы

Аффилиация

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