eComp_op_eq

Mathlib.CategoryTheory.Enriched.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.eComp_op_eq

Lean4

/-- Unfold the definition of composition in the enriched opposite category. -/
@[reassoc]
theorem eComp_op_eq {C : Type u} [EnrichedCategory V C] (x y z : Cᵒᵖ) :
    eComp V z y x = (β_ _ _).hom ≫ eComp V x.unop y.unop z.unop :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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