from_self

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsTerminal.from_self

English

The map from a terminal object to itself is the identity: t.from X = id_X.

Русский

Отображение из терминального объекта в сам объект есть тождество: t.from X = id X.

LaTeX

$$$t.from X = \mathrm{id}_X$$$

Lean4

@[simp]
theorem from_self {X : C} (t : IsTerminal X) : t.from X = 𝟙 X :=
  t.hom_ext _ _

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

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

Разделы

Аффилиация

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