of_isIso_comp_right

Mathlib.CategoryTheory.Iso

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

← MathLib Explorer

English

If g is an isomorphism and f ≫ g is an isomorphism, then f is an isomorphism.

Русский

Если g изоморфизм и f ≫ g изоморфизм, то f изоморфизм.

LaTeX

$$$IsIso g\to IsIso (f\gg g)\to IsIso f$$$

Lean4

theorem of_isIso_comp_right {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsIso (f ≫ g)] : IsIso f :=
  by
  rw [← comp_id f, ← hom_inv_id g, ← assoc]
  infer_instance

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

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

Разделы

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

Аффилиация

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