card_pi — Mathlib

English

The cardinality of the dependent function space ∀ i, α(i) equals the product over i of the cardinalities of α(i).

Русский

Кардинальность пространства зависимых функций ∀ i, α(i) равна произведению по i от кардинальности α(i).

LaTeX

$$$\\operatorname{card}(\\forall i, \\alpha(i)) = \\prod_{i} \\operatorname{card}(\\alpha(i))$$$

Lean4

@[simp]
theorem card_pi (s : Finset ι) (t : ∀ i, Finset (α i)) : #(s.pi t) = ∏ i ∈ s, #(t i) :=
  Multiset.card_pi _ _

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