of_isIso_comp_left

Mathlib.CategoryTheory.Iso

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

← MathLib Explorer

English

If f and g are morphisms with f an isomorphism and f ≫ g an isomorphism, then g is an isomorphism.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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