card_product — Mathlib

English

The cardinality of the product s ×ˢ t equals the product of the cardinalities: card(s ×ˢ t) = card(s) · card(t).

Русский

Число элементов в произведении равно произведению чисел элементов каждого множества: card(s ×ˢ t) = card(s) · card(t).

LaTeX

$$$\mathrm{card}(s \times^{\mathrm{SProd}} t) = \mathrm{card}(s) \cdot \mathrm{card}(t)$$$

Lean4

@[simp]
theorem card_product : card (s ×ˢ t) = card s * card t := by simp [SProd.sprod, product]

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