instPProd — Mathlib

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

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