mkFunctor_obj_left

Mathlib.CategoryTheory.Join.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.mkFunctor_obj_left

English

In the constructed functor MkFunctor, the image of a left object c is F.obj c.

Русский

В сконструированном функторе MkFunctor образ левого объекта c равен F.obj c.

LaTeX

$$$(\\mathrm{MkFunctor}\ F\ G\ \\alpha).obj(\\mathrm{left}\ c) = F.obj\\ c$$$

Lean4

@[simp]
theorem mkFunctor_obj_left (c : C) : (mkFunctor F G α).obj (left c) = F.obj c :=
  rfl

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

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

Разделы

Аффилиация

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