i_w

Mathlib.CategoryTheory.Retract

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

English

In a RetractArrow, the left leg and right leg satisfy the compatibility condition: i.left ≫ g = f ≫ i.right.

Русский

Для RetractArrow выполняется совместимость: i.left ∘ g = f ∘ i.right.

LaTeX

$$$h.i.left \circ g = f \circ h.i.right$$$

Lean4

@[reassoc]
theorem i_w : h.i.left ≫ g = f ≫ h.i.right :=
  h.i.w

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

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

Разделы

Аффилиация

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