mkFunctor_obj_right

Mathlib.CategoryTheory.Join.Basic

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

English

For every object d in D, the right component of mkFunctor F G α evaluated at right d is G.obj d.

Русский

Для каждого объекта d ∈ D правая компонента mkFunctor F G α, применённая к right d, равна G.obj d.

LaTeX

$$$ (\mathrm{mkFunctor} F G \alpha).\mathrm{obj}(\mathrm{right}\; d) = G.\mathrm{obj}(d) $$$

Lean4

@[simp]
theorem mkFunctor_obj_right (d : D) : (mkFunctor F G α).obj (right d) = G.obj d :=
  rfl

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

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

Разделы

Аффилиация

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