subterminals_thin

Mathlib.CategoryTheory.Subterminal

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

English

Between any two subterminal objects X, Y, there is at most one morphism X → Y.

Русский

Для любых подтерминальных объектов X, Y существует не более одного морфизма X → Y.

LaTeX

$$For all X,Y ∈ Subterminals(C), \operatorname{Subsingleton}(\mathrm{Hom}(X,Y))$$

Lean4

instance subterminals_thin (X Y : Subterminals C) : Subsingleton (X ⟶ Y) :=
  ⟨fun f g => Y.2 f g⟩

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

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

Разделы

Аффилиация

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