univ_product_univ

Mathlib.Data.Fintype.Prod

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

English

The universal product of univ with univ equals univ: univ × univ = univ.

Русский

Произведение единичного множества с единичным равно единичному.

LaTeX

$$$\\mathrm{univ} \\times\\!\\mathrm{univ} = (\\mathrm{univ} : \\mathrm{Finset}(\\alpha \\times \\beta))$$$

Lean4

@[simp]
theorem univ_product_univ : univ ×ˢ univ = (univ : Finset (α × β)) :=
  rfl

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

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

Разделы

Аффилиация

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