subsingleton_iso

Mathlib.CategoryTheory.Thin

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

English

For any X,Y in a thin category C, Iso(X,Y) is a singleton.

Русский

Для любых X,Y в тонкой категории Iso(X,Y) имеет единственный элемент.

LaTeX

$$∀ X Y ∈ C, Subsingleton (X ≅ Y)$$

Lean4

instance subsingleton_iso {X Y : C} : Subsingleton (X ≅ Y) :=
  ⟨by
    intro i₁ i₂
    ext1
    subsingleton⟩

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

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

Разделы

Аффилиация

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