inv_inv

Mathlib.CategoryTheory.Iso

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

English

The inverse of the inverse of an isomorphism is the original morphism.

Русский

Обратное к обратному изоморфизму даёт исходный морфизм.

LaTeX

$$$inv$inv\ f$ = f$$$

Lean4

@[simp]
theorem inv_inv [IsIso f] : inv (inv f) = f :=
  by
  apply inv_eq_of_hom_inv_id
  simp

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

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

Разделы

Аффилиация

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