functorMapSrc_functorObjTop

Mathlib.CategoryTheory.SmallObject.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.functorMapSrc_functorObjTop

Lean4

@[reassoc (attr := simp)]
theorem functorMapSrc_functorObjTop : functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ τ.left :=
  by
  ext ⟨i, t, b, w⟩
  simp [ι_functorMapSrc_assoc f τ i t b w _ rfl]

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

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

Разделы

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

Аффилиация

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