mul_def

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.mul_def

English

The cardinality of a product type equals the product of the cardinals: |α| · |β| = |α × β|.

Русский

Кардинал произведения типов равен произведению кардиналов: |α| · |β| = |α × β|.

LaTeX

$$$|\alpha| \cdot |\beta| = |\alpha \times \beta|$$$

Lean4

theorem mul_def (α β : Type u) : #α * #β = #(α × β) :=
  rfl

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

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

Разделы

Аффилиация

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