hasFiniteProducts_of_hasFiniteBiproducts

English

If a category C has finite biproducts, then it has finite products.

Русский

Если в категории C существуют конечные бипродукты, то существуют и конечные произведения.

LaTeX

$$$\text{HasFiniteBiproducts}(C) \Rightarrow \text{HasFiniteProducts}(C)$$$

Lean4

instance (priority := 100) hasFiniteProducts_of_hasFiniteBiproducts [HasFiniteBiproducts C] : HasFiniteProducts C where
  out _ := ⟨fun _ => hasLimit_of_iso Discrete.natIsoFunctor.symm⟩

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