card_finsupp — Mathlib

English

If ι is finite and α is finite, then the number of finitely supported maps ι →₀ α equals card α to the power card ι; i.e., card(ι →₀ α) = card α ^ card ι.

Русский

Если ι и α конечны, то число конечноподдерживаемых отображений ι →₀ α равно card(α)^{card(ι)}.

LaTeX

$$$\\operatorname{card}(ι \\to_0 α) = \\operatorname{card}(α)^{\\operatorname{card}(ι)}$$$

Lean4

@[simp]
theorem card_finsupp : card (ι →₀ α) = card α ^ card ι := by simp [card_congr Finsupp.equivFunOnFinite]

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