inlCompInlCompAssociator — Mathlib

English

There is a canonical isomorphism inl_ (C ⊕ D) E ⋙ associator C D E ≅ inl_ C (D ⊕ E).

Русский

Существует каноническое изоморфное отображение inl_ (C ⊕ D) E ⋙ ассоциатор C D E ≅ inl_ C (D ⊕ E).

LaTeX

$$CategoryTheory.Sum.inl_ (Sum C D) E ⋅ associator C D E ≅ inl_ C (Sum D E)$$

Lean4

/-- Further characterizing the composition of the associator and the left inclusion. -/
@[simps!]
def inlCompInlCompAssociator : inl_ C D ⋙ inl_ (C ⊕ D) E ⋙ associator C D E ≅ inl_ C (D ⊕ E) :=
  isoWhiskerLeft (inl_ _ _) (inlCompAssociator C D E) ≪≫ Functor.inlCompSum' _ _

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