English
If X --hom--> Y and Y --hom'--> Z with appropriate inverses, then the transitive composite of the two isomorphisms equals the isomorphism given by the composite arrows.
Русский
Если есть последовательности изomорфизмов ⟨hom, inv⟩ и ⟨hom', inv'⟩, то их свободное умножение даёт изоморфизм с композициями hom≫hom' и inv'≫inv.
LaTeX
$$$\\text{Iso.trans}\\langle hom, inv, hom\\_inv\\_id, inv\\_hom\\_id\\rangle \\; \\langle hom', inv', hom\\_inv\\_id', inv\\_hom\\_id'\\rangle = \\langle hom \\gg M hom', inv' \\gg inv, hom\\_inv\\_id'', inv\\_hom\\_id''\\rangle$$$
Lean4
@[simp, grind =]
theorem trans_mk {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id) (inv_hom_id) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y)
(hom_inv_id') (inv_hom_id') (hom_inv_id'') (inv_hom_id'') :
Iso.trans ⟨hom, inv, hom_inv_id, inv_hom_id⟩ ⟨hom', inv', hom_inv_id', inv_hom_id'⟩ =
⟨hom ≫ hom', inv' ≫ inv, hom_inv_id'', inv_hom_id''⟩ :=
rfl
