card_piFinset_const — Mathlib

English

For s a finite set and n a natural number, the cardinality of piFinset over the constant function equals |s|^n.

Русский

Для конечного множества s и числа n кардинальность piFinset для константной функции равна |s|^n.

LaTeX

$$$\\#(\\pi\\mathrm{Finset}\\, (\\lambda _ : \\mathrm{Fin}\\ n \\mapsto s)) = \\#s^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_piFinset`. -/
theorem card_piFinset_const {α : Type*} (s : Finset α) (n : ℕ) : #(piFinset fun _ : Fin n ↦ s) = #s ^ n := by simp

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