English
If α is finite and for every a ∈ α, β(a) is finite, then the dependent product ∏_{a∈α} β(a) is finite.
Русский
Если α конечно и для каждого a ∈ α множество β(a) конечно, то зависимый произведение ∏_{a∈α} β(a) конечно.
LaTeX
$$$ [\\text{Finite }\\alpha] \\,[\\forall a, \\text{Finite}(\\beta(a))] \\Rightarrow \\text{Finite}(\\prod_{a:\\alpha} \\beta(a)) $$$
Lean4
instance {α β : Sort*} [Finite α] [Finite β] : Finite (PProd α β) :=
of_equiv _ Equiv.pprodEquivProdPLift.symm