inv_hom

Mathlib.CategoryTheory.Iso

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

English

For an isomorphism f: X ≅ Y, the inverse of the morphism part equals the inverse component: inv(f.hom) = f.inv.

Русский

Для изоморфизма f: X ≅ Y обратная к морфизму равна компоненте обратного: inv(f.hom) = f.inv.

LaTeX

$$inv f.hom = f.inv$$

Lean4

@[simp]
theorem inv_hom (f : X ≅ Y) : inv f.hom = f.inv :=
  by
  apply inv_eq_of_hom_inv_id
  simp

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

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

Разделы

Аффилиация

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