instSubsingletonHom

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.WalkingSpan.instSubsingletonHom

English

All morphisms in WalkingSpan are unique; the hom-sets in WalkingSpan are singleton.

Русский

Все морфизмы в WalkingSpan уникальны; гомоморфизмы в WalkingSpan образуют единичное множество.

LaTeX

$$$ \\forall X,Y \\in \\mathrm{WalkingSpan},\\; X\\to Y \\text{ is unique} $$$

Lean4

instance (X Y : WalkingSpan) : Subsingleton (X ⟶ Y) := by constructor; intro a b; simp [eq_iff_true_of_subsingleton]

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

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

Разделы

Аффилиация

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