associator_inv_fst_fst

Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst

English

The inverse associator composed with fst twice yields fst.

Русский

Обратный ассоциатор, после fst дважды, даёт fst.

LaTeX

$$$(\alpha_{X Y Z})^{\mathrm{inv}} \circ \mathrm{prod.fst} \circ \mathrm{prod.fst} = \mathrm{prod.fst}$$$

Lean4

@[reassoc]
theorem associator_inv_fst_fst (X Y Z : C) : (α_ X Y Z).inv ≫ prod.fst ≫ prod.fst = prod.fst := by simp [associator_inv]

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

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

Разделы

Аффилиация

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