limit — Mathlib

English

If P is closed under isomorphisms and whenever a J-shaped diagram F in C has a limit, and every object F(j) lies in P, then the limit lies in P; hence P is closed under limits of shape J

Русский

Если P замкнуто по изоморфизмам и для любого диаграммного рисунка F по форме J существует предел, если все объекты F(j) принадлежат P, то предел принадлежит P; значит, P замкнуто по пределам формы J

LaTeX

$$$\\forall F: J \\to C,\\; [\\text{HasLimit } F] \\Rightarrow (\\forall j, P(F(j))\\Rightarrow P(\\lim F))$$$

Lean4

protected theorem limit (h : ClosedUnderLimitsOfShape J P) {F : J ⥤ C} [HasLimit F] :
    (∀ j, P (F.obj j)) → P (limit F) :=
  h (limit.isLimit _)

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