English
If α is finite and every β(a) is finite, then the space of all functions a ↦ β(a) is finite.
Русский
Если α конечно и для каждого a ∈ α β(a) конечно, то множество функций a ↦ β(a) конечно.
LaTeX
$$$ [\\text{Finite }\\alpha] \\,[\\forall a: \\alpha, \\text{Finite}(\\beta(a))] \\Rightarrow \\text{Finite}(\\{ f: \\alpha \\to \\beta(a) \\mid a \\in \\alpha \\}) $$$
Lean4
instance finite {α : Sort*} {β : α → Sort*} [Finite α] [∀ a, Finite (β a)] : Finite (∀ a, β a) := by
classical
haveI := Fintype.ofFinite (PLift α)
haveI := fun a => Fintype.ofFinite (PLift (β a))
exact Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a))) (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
