inverseAssociator_obj_inr_inl

Mathlib.CategoryTheory.Sums.Associator

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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