inv_hom_id_right

Mathlib.CategoryTheory.Comma.Arrow

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

English

For Iso e, e.inv.right ≫ e.hom.right = id on g.right.

Русский

Для изоморфизма e: e.inv.right ≫ e.hom.right = id_{g.right}.

LaTeX

$$$e.inv.right \circ e.hom.right = \mathrm{Id}_{g.right}$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_id_right (e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 _ := by rw [← comp_right, e.inv_hom_id, id_right]

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

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

Разделы

Аффилиация

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