hasLimit — Mathlib

English

Let J be a diagram shape and X an object of a category C. If pres is a LimitPresentation J X, then the diagram pres.diag has a limit; equivalently, there exists a limit cone over pres.diag. In particular, the universal cone is the one provided by pres.isLimit.

Русский

Пусть J — форма диаграммы, X — объект в категории C. Если pres является презентацией предела для J над X, то диаграмма pres.diag имеет предел; эквивалентно, существует предел-конус над diagrampres.diag. В частности, универсальный конус задаётся pres.isLimit.

LaTeX

$$$$\exists t:\mathrm{Cone}(\mathrm{pres.diag}),\ \mathrm{IsLimit}(t).$$$$

Lean4

theorem hasLimit (pres : LimitPresentation J X) : HasLimit pres.diag :=
  ⟨_, pres.isLimit⟩

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