associator_inv_app_apply — Mathlib

English

The inverse of the associator on a triple tensor acts by nested pairing to reflect the inverse associator structure.

Русский

Обратная ассоциаторная карта на тройном тензоре действует по вложенным парам так, чтобы отразить структуру обратного ассоциатора.

LaTeX

$$$ (\alpha_{K,L,M}).inv.app Δ x = ⟨⟨x.1, x.2.1⟩, x.2.2⟩ $$$

Lean4

@[simp]
theorem associator_inv_app_apply (K L M : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ L ⊗ M).obj Δ) :
    (α_ K L M).inv.app Δ x = ⟨⟨x.1, x.2.1⟩, x.2.2⟩ :=
  rfl

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