mkOfHomFunctors_mapFunctor

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PrelaxFunctor.mkOfHomFunctors_mapFunctor

Lean4

@[simp]
theorem mkOfHomFunctors_mapFunctor (F : B → C) (F' : (a : B) → (b : B) → (a ⟶ b) ⥤ (F a ⟶ F b)) (a b : B) :
    (mkOfHomFunctors F F').mapFunctor a b = F' a b :=
  rfl

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

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

Разделы

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

Аффилиация

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