inv_left_hom_right

Mathlib.CategoryTheory.Comma.Arrow

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

English

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

Русский

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

LaTeX

$$$\operatorname{inv}(sq.left) \circ f.hom \circ sq.right = g.hom$$$

Lean4

theorem inv_left_hom_right [IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.hom := by simp only [w, IsIso.inv_comp_eq]

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

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

Разделы

Аффилиация

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