isSubterminal_of_isTerminal — Mathlib

English

Let T be a terminal object in a category. Then T is subterminal, i.e., for every object X there is at most one morphism X → T.

Русский

Пусть T — терминальный объект в категории. Тогда T является подтерминальным, то есть из каждого объекта X существует не более одного морфизма X → T.

LaTeX

$$$\operatorname{IsTerminal}(T) \rightarrow \operatorname{IsSubterminal}(T)$$$

Lean4

theorem isSubterminal_of_isTerminal {T : C} (hT : IsTerminal T) : IsSubterminal T := fun _ _ _ => hT.hom_ext _ _

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