card_product

Mathlib.Data.Finset.Prod

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

English

Let S and T be finite sets. Then |S × T| = |S| · |T|.

Русский

Пусть S и T — конечные множества. Тогда |S × T| = |S| · |T|.

LaTeX

$$$|S \\\\times T| = |S| \\\\cdot |T|$$$

Lean4

@[simp]
theorem card_product (s : Finset α) (t : Finset β) : card (s ×ˢ t) = card s * card t :=
  Multiset.card_product _ _

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

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

Разделы

Аффилиация

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