associator_obj_inr

Mathlib.CategoryTheory.Sums.Associator

URI: https://scilib.ai/kg/mathlib#CategoryTheory.sum.associator_obj_inr

English

The associator sends inr X to inr(inr X).

Русский

Ассоциатор отображает inr X в inr(inr X).

LaTeX

$$((\operatorname{associator}_{C,D,E}).\mathrm{obj})(\mathrm{inr} X) = \mathrm{inr}(\mathrm{inr} X)$$

Lean4

@[simp]
theorem associator_obj_inr (X) : (associator C D E).obj (inr X) = inr (inr X) :=
  rfl

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

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

Разделы

Аффилиация

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