of_AB5Star — Mathlib

English

A category with finite biproducts and finite limits is AB4Star if AB5Star holds; the countable variant follows similarly.

Русский

Категория с конечными бинопродуктами и пределами AB4Star, если AB5Star выполнено; аналогично и для счетной версии.

LaTeX

$$$\\operatorname{AB4StarOfSize}(C) \\Leftarrow \\operatorname{AB5StarOfSize}(C)$$$

Lean4

/-- A category with finite biproducts and finite limits is AB4 if it is AB5. -/
theorem of_AB5Star [HasCofilteredLimitsOfSize.{w, w} C] [AB5StarOfSize.{w, w} C] : AB4StarOfSize.{w} C where
  ofShape _ := hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op _ _

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