toEquiv_comp — Mathlib

English

For isomorphisms f: X ≅ Y and g: Y ≅ Z, the equivalence associated to the composite matches the composite of the equivalences: (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv.

Русский

Для изоморфизмов f: X ≅ Y и g: Y ≅ Z соответствующая эквивалентность для композиции равна композиции эквивалентностей: (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv.

LaTeX

$$$ (f \\llap{\\!} \\gg g).toEquiv = f.toEquiv.trans g.toEquiv $$$

Lean4

@[simp]
theorem toEquiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) : (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv :=
  rfl

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