inverseAssociator_obj_inl

Mathlib.CategoryTheory.Sums.Associator

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

English

The inverse associator sends inl X to inl (inl X).

Русский

Обратный ассоциатор отображает inl X в inl (inl X).

LaTeX

$$inverseAssociator :\n \mathrm{obj}(\mathrm{inl}(X)) = \mathrm{inl}(\mathrm{inl}(X))$$

Lean4

@[simp]
theorem inverseAssociator_obj_inl (X) : (inverseAssociator C D E).obj (inl X) = inl (inl X) :=
  rfl

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

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

Разделы

Аффилиация

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