trans_assoc — Mathlib

English

The composition of three isomorphisms is associative: (α.trans β).trans γ = α.trans (β.trans γ).

Русский

Сопоставимость композиции трех изоморфизмов: (α.trans β).trans γ = α.trans (β.trans γ).

LaTeX

$$$\\forall {C} [\\mathrm{Category}(C)], {X Y Z Z'} (\\alpha : X \\cong Y) (\\beta : Y \\cong Z) (\\gamma : Z \\cong Z'), \\\\ (\\alpha.\\trans \\beta).\\trans \\gamma = \\alpha.\\trans (\\beta.\\trans \\gamma)$$$

Lean4

@[simp, grind _=_]
theorem trans_assoc {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') : (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ := by ext;
  simp only [trans_hom, Category.assoc]

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