retract_left

Mathlib.CategoryTheory.Retract

URI: https://scilib.ai/kg/mathlib#CategoryTheory.RetractArrow.retract_left

English

In a RetractArrow, the left component of i and the left leg of r compose to the identity on the left object: i.left ≫ r.left = 𝟙 X.

Русский

Для RetractArrow: i.left ∘ r.left = 𝟙 X.

LaTeX

$$$i_{left} \circ r_{left} = \mathrm{Id}_X$$$

Lean4

@[reassoc (attr := simp)]
theorem retract_left : h.i.left ≫ h.r.left = 𝟙 X :=
  h.left.retract

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

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

Разделы

Аффилиация

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