comp_app'

Mathlib.CategoryTheory.Bicategory.Modification.Oplax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Oplax.OplaxTrans.Modification.comp_app'

Lean4

/-- Version of `Modification.comp_app` using category notation -/
@[simp]
theorem comp_app' {X : B} {F G : OplaxFunctor B C} {α β γ : F ⟶ G} (m : α ⟶ β) (n : β ⟶ γ) :
    (m ≫ n).app X = m.app X ≫ n.app X :=
  rfl

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

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

Разделы

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

Аффилиация

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