instHasTerminal

Mathlib.CategoryTheory.Limits.Preorder

URI: https://scilib.ai/kg/mathlib#Preorder.instHasTerminal

English

A preorder with a top element yields a terminal object in its associated category.

Русский

Порядок с верхним элементом порождает терминальный объект в соответствующей категории.

LaTeX

$$$ [\\text{HasTerminal } C] \\Rightarrow \\text{HasTerminal }(C)$$$

Lean4

instance : HasTerminal C :=
  hasTerminal_of_unique ⊤

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

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

Разделы

Аффилиация

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