w_mk_right

Mathlib.CategoryTheory.Comma.Arrow

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

English

The w relation of a comma square shows compatibility of components with the right side.

Русский

Связь w для квадрата заполняет совместимость левых и правых частей.

LaTeX

$$$sq.left ≫ g.hom = f.hom ≫ sq.right$$$

Lean4

@[reassoc (attr := simp)]
theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) : sq.left ≫ g = f.hom ≫ sq.right :=
  sq.w

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

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

Разделы

Аффилиация

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