card_pi_const — Mathlib

English

For a finite type α and n, the cardinality of the function space Fin n → α equals card(α)^n.

Русский

Для конечного типа α и натурального числа n кардинальность пространства функций Fin n → α равна card(α)^n.

LaTeX

$$$|\\mathrm{Fin}\\ n \\to \\alpha| = |\\alpha|^n$$$

Lean4

/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_pi`. -/
theorem card_pi_const (α : Type*) [Fintype α] (n : ℕ) : card (Fin n → α) = card α ^ n :=
  card_piFinset_const _ _

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