hasFiniteLimits — Mathlib

English

In an Abelian category, finite limits exist. In particular, the category has all finite limits, i.e., has equalizers, pullbacks, finite products, and so on.

Русский

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

LaTeX

$$$\\\\forall C \\\\text{ abelian }, \\\\mathrm{HasFiniteLimits}(C)$$

Lean4

instance (priority := 100) hasFiniteLimits : HasFiniteLimits C :=
  Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products

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