nonempty_iso_refl

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.nonempty_iso_refl

English

For any object X in a category C, there exists a nonempty isomorphism X ≅ X (identity isomorphism).

Русский

Для любого объекта X в категории C существует ненулевой изоморфизм X ≅ X (идентичный изоморфизм).

LaTeX

$$$ \\forall X \\in C, \\ Nonempty(X \\cong X) $$$

Lean4

theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) :=
  ⟨default⟩

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

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

Разделы

Аффилиация

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