instHasTerminal

Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

English

There exists a terminal object in SimplexCategory; namely ⟦0⟧.

Русский

Существование терминального объекта в SimplexCategory; например ⟦0⟧.

LaTeX

$$$\\text{HasTerminal}(\\mathrm{SimplexCategory})$ with terminal object $\\langle 0 \\rangle$.$$

Lean4

instance : HasTerminal SimplexCategory :=
  IsTerminal.hasTerminal isTerminalZero

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

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

Разделы

Аффилиация

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