inverseAssociator_obj_inr_inr

Mathlib.CategoryTheory.Sums.Associator

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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