inv_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.inv_id

English

The inverse of the identity morphism is itself.

Русский

Обратная единичному морфизму равна самому морфизму.

LaTeX

$$$inv(𝟙 X) = 𝟙 X$$$

Lean4

@[simp]
theorem inv_id : inv (𝟙 X) = 𝟙 X := by
  apply inv_eq_of_hom_inv_id
  simp

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

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

Разделы

Аффилиация

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