card_pi — Mathlib

English

For a family of finite types α i, the cardinality of the space of all functions i → α(i) equals the product of the cardinals.

Русский

Для семейства конечных типов α_i кардинальность пространства функций i → α(i) равна произведению кардиналостей α_i.

LaTeX

$$$\\operatorname{card}\\bigl(\\,(i \\mapsto \\alpha(i))\\bigr) = \\prod_{i} \\operatorname{card}(\\alpha(i))$$$

Lean4

@[simp]
theorem card_pi [∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i) :=
  card_piFinset _

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