hasProducts_of_finite_and_cofiltered

English

Dual to the coproduct result: if C has finite products and HasCofilteredLimitsOfSize, then C has finite products; i.e., HasProducts.

Русский

Двойственный результат: если в C имеются конечные произведения и HasCofilteredLimitsOfSize, то C имеет конечные произведения; т.е. HasProducts.

LaTeX

$$$$ \text{hasProducts_of_finite_and_cofiltered} \;:\; [HasFiniteProducts\, C] \to [HasCofilteredLimitsOfSize\{w,w\}\, C] \to [HasProducts\, C]. $$$$

Lean4

theorem hasProducts_of_finite_and_cofiltered [HasFiniteProducts C] [HasCofilteredLimitsOfSize.{w, w} C] :
    HasProducts.{w} C :=
  have : HasCoproducts.{w} Cᵒᵖ := hasCoproducts_of_finite_and_filtered
  hasProducts_of_opposite

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