hasTerminal

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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

English

A zero object is terminal; for every X there is a unique arrow X → 0.

Русский

Нулевой объект является терминальным; для каждого X существует уникальная стрелка X → 0.

LaTeX

$$\\forall X, \\exists! f: X \\to 0$$

Lean4

/-- A zero object is in particular terminal. -/
instance (priority := 10) hasTerminal : HasTerminal C :=
  hasTerminal_of_unique 0

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

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

Разделы

Аффилиация

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