instProd — Mathlib

English

If α and β are finite types, then their Cartesian product α × β is finite.

Русский

Если α и β конечны, то их декартово произведение α × β конечно.

LaTeX

$$$ [\\text{Finite }\\alpha] \\,[\\text{Finite }\\beta] \\Rightarrow \\text{Finite}(\\alpha \\times \\beta) $$$

Lean4

instance [Finite α] [Finite β] : Finite (α × β) :=
  by
  haveI := Fintype.ofFinite α
  haveI := Fintype.ofFinite β
  infer_instance

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