English
Let ι be a finite index set and t(i) a finite set for each i. Then the set of all choice functions f with f(i) ∈ t(i) for every i is finite.
Русский
Пусть ι — конечный индексный набор, и для каждого i ∈ ι задано множество t(i), конечное. Тогда множество всех функций выбора f, удовлетворяющих f(i) ∈ t(i) для всех i, конечно.
LaTeX
$$$\\operatorname{Finite}\\left(\\prod_{i \\in \\iota} t(i)\\right).$$$
Lean4
/-- Finite product of finite sets is finite -/
theorem pi (ht : ∀ i, (t i).Finite) : (pi univ t).Finite :=
by
cases nonempty_fintype ι
lift t to ∀ d, Finset (κ d) using ht
classical
rw [← Fintype.coe_piFinset]
apply Finset.finite_toSet
