id_app'

Mathlib.CategoryTheory.Bicategory.Modification.Oplax

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

Lean4

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

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

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

Разделы

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

Аффилиация

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