isIso_right

Mathlib.CategoryTheory.Comma.Arrow

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.isIso_right

← MathLib Explorer

English

If sq : f ⟶ g is an isomorphism, then sq.right is an isomorphism in T.

Русский

Если sq : f ⟶ g является изоморфизмом, то sq.right — изоморфизм в T.

LaTeX

$$$\text{IsIso}(sq.right)$$$

Lean4

instance isIso_right [IsIso sq] : IsIso sq.right where
  out := by
    apply Exists.intro (inv sq).right
    simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id]
    simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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