hasFiniteProducts_of_hasFiniteLimits

English

If a category has all products, then it has finite products; in particular, for every finite index set I there exists a product of the corresponding objects.

Русский

Если в категории существуют все произведения, то существуют и конечные произведения; для любого конечного множества индексов I существует произведение соответствующих объектов.

LaTeX

$$$[\text{HasProducts } C] \Rightarrow \operatorname{HasFiniteProducts}(C)$$$

Lean4

/-- If `C` has finite limits then it has finite products. -/
instance (priority := 10) hasFiniteProducts_of_hasFiniteLimits [HasFiniteLimits C] : HasFiniteProducts C :=
  ⟨fun _ => inferInstance⟩

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