isIso_hom

Mathlib.CategoryTheory.Iso

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

English

For an isomorphism e: X ≅ Y, the inverse e.inv is also an isomorphism.

Русский

Для изоморфизма e: X ≅ Y обратный e.inv также является изоморфизмом.

LaTeX

$$IsIso e.inv$$

Lean4

theorem isIso_hom (e : X ≅ Y) : IsIso e.hom :=
  ⟨e.inv, by simp only [hom_inv_id], by simp⟩

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

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

Разделы

Аффилиация

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