hasTerminal

Mathlib.CategoryTheory.Limits.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.hasTerminal

English

If G is faithful and full, then CostructuredArrow G X has a terminal object.

Русский

Если G является инъективно полнофункциональным, то CostructuredArrow G X имеет терминал.

LaTeX

$$$\\text{HasTerminal}(\\mathrm{CostructuredArrow}\\, G\\, X)$$$

Lean4

instance hasTerminal [G.Faithful] [G.Full] {Y : A} : HasTerminal (CostructuredArrow G (G.obj Y)) :=
  CostructuredArrow.mkIdTerminal.hasTerminal

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru