associatorIsEquivalence

Mathlib.CategoryTheory.Products.Associator

URI: https://scilib.ai/kg/mathlib#CategoryTheory.prod.associatorIsEquivalence

English

The associator is an equivalence of categories; hence ((C × D) × E) ≌ (C × (D × E)).

Русский

Ассоциатор является эквивалентностью категорий; следовательно, ((C × D) × E) ≌ (C × (D × E)).

LaTeX

$$$\text{associativity }\,\text{IsEquivalence}$$$

Lean4

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

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

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

Разделы

Аффилиация

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