associatorIsEquivalence — Mathlib

English

For any categories C, D, E, the associator functor (C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E) is an equivalence of categories.

Русский

Для любых категорий C, D, E композиционный функтор ассоциатора между (C ⊕ D) ⊕ E и C ⊕ (D ⊕ E) является эквивалентностью категорий.

LaTeX

$$$$ \text{associator}_{C D E} : (C \oplus D) \oplus E \stackrel{\sim}{\to} C \oplus (D \oplus E) \text{ is an equivalence.} $$$$

Lean4

instance associatorIsEquivalence : (associator C D E).IsEquivalence :=
  (by infer_instance : (associativity C D E).functor.IsEquivalence)

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