toIsometryEquiv_trans — Mathlib

English

The toIsometryEquiv map respects composition: for isomorphisms e: X ≅ Y and f: Y ≅ Z, toIsometryEquiv (e ≪≫ f) equals e.toIsometryEquiv.trans f.toIsometryEquiv.

Русский

Сопоставление toIsometryEquiv сохраняет композицию: для изоморфизмов e: X ≅ Y и f: Y ≅ Z, toIsometryEquiv (e ≪≫ f) = e.toIsometryEquiv.trans f.toIsometryEquiv.

LaTeX

$$$\\mathrm{toIsometryEquiv}(e \\circ f) = (\\mathrm{toIsometryEquiv}(e)) \\circ (\\mathrm{toIsometryEquiv}(f))$$$

Lean4

@[simp]
theorem toIsometryEquiv_trans (e : X ≅ Y) (f : Y ≅ Z) :
    toIsometryEquiv (e ≪≫ f) = e.toIsometryEquiv.trans f.toIsometryEquiv :=
  rfl

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