isSubterminal_of_terminal

Mathlib.CategoryTheory.Subterminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isSubterminal_of_terminal

English

If a category has a terminal object, then the terminal object ⊤_C is subterminal.

Русский

Если у категории есть терминальный объект, то ⊤_C является подтерминальным.

LaTeX

$$$\operatorname{IsSubterminal}(\top_C)$$$

Lean4

theorem isSubterminal_of_terminal [HasTerminal C] : IsSubterminal (⊤_ C) := fun _ _ _ => by subsingleton

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

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

Разделы

Аффилиация

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