isTerminalZero

Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

English

The object ⟦0⟧ is terminal in SimplexCategory.

Русский

Объект ⟦0⟧ является терминальным в SimplexCategory.

LaTeX

$$$\\text{IsTerminal}(\\langle 0 \\rangle).$$$

Lean4

/-- The object `⦋0⦌` is terminal in `SimplexCategory`. -/
def isTerminalZero : IsTerminal (⦋0⦌ : SimplexCategory) :=
  IsTerminal.ofUnique ⦋0⦌

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

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

Разделы

Аффилиация

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