ncard_prod

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.ncard_prod

English

The cardinality of the Cartesian product equals the product of cardinalities: |s × t| = |s| · |t|.

Русский

Кардинал произведения множеств равен произведению кардиналов: |s × t| = |s| · |t|.

LaTeX

$$$ (s \times \; t).ncard = s.ncard \cdot t.ncard $$$

Lean4

@[simp]
theorem ncard_prod {s : Set α} {t : Set β} : (s ×ˢ t).ncard = s.ncard * t.ncard := by simp [ncard, ENat.toNat_mul]

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

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

Разделы

Аффилиация

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