hasColimit — Mathlib

English

For a colimit presentation pres, HasColimit pres.diag holds, i.e., the diagram pres.diag has a colimit with the given universal property.

Русский

Для презентации колимита pres, выполняется условие HasColimit pres.diag: диаграмма pres.diag имеет колимит с заданным универсальным свойством.

LaTeX

$$$ \\text{HasColimit}( pres.diag )$.$$

Lean4

theorem hasColimit (pres : ColimitPresentation J X) : HasColimit pres.diag :=
  ⟨_, pres.isColimit⟩

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