isIso_iff_isIso_of_isIso

Mathlib.CategoryTheory.Comma.Arrow

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

← MathLib Explorer

English

For sq : mk f ⟶ mk g that is an isomorphism, IsIso f ↔ IsIso g.

Русский

Для sq : mk f ⟶ mk g, являющегося изоморфизмом, IsIso f ↔ IsIso g.

LaTeX

$$$\text{IsIso}(f) \iff \text{IsIso}(g)$$$

Lean4

theorem isIso_iff_isIso_of_isIso {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (sq : mk f ⟶ mk g) [IsIso sq] :
    IsIso f ↔ IsIso g :=
  isIso_hom_iff_isIso_hom_of_isIso sq

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

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

Разделы

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

Аффилиация

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