comp_isIso

Mathlib.CategoryTheory.Iso

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

English

If f and h are isomorphisms, then their composition f ≫ h is an isomorphism.

Русский

Если f и h — изоморфизмы, то их композиция f ≫ h — изоморфизм.

LaTeX

$$IsIso (f ≫ h)$$

Lean4

instance (priority := 900) comp_isIso [IsIso f] [IsIso h] : IsIso (f ≫ h) :=
  (asIso f ≪≫ asIso h).isIso_hom

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

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

Разделы

Аффилиация

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