left_hom_inv_right

Mathlib.CategoryTheory.Comma.Arrow

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

English

For IsIso sq, left ≫ g.hom ≫ inv sq.right = f.hom.

Русский

Для изоморфизма sq: left ≫ g.hom ≫ inv sq.right = f.hom.

LaTeX

$$$\,sq.left \circ g.hom \circ (inv\,sq.right) = f.hom$$$

Lean4

theorem left_hom_inv_right [IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom := by
  simp only [← Category.assoc, IsIso.comp_inv_eq, w]

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

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

Разделы

Аффилиация

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