inrCompInlCompAssociator — Mathlib

English

There is a canonical isomorphism for composing inl with inl and the associator.

Русский

Существует каноническое изоморфизм при композиции inl и inl и ассоциатора.

LaTeX

$$inl C D ⋙ inl_ (C ⊕ D) E ⋙ associator C D E ≅ inl C (D ⊕ E)$$

Lean4

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

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