eqToHom_right — Mathlib

English

If X and Y are equal as objects in StructuredArrow S T, then the right component of the canonical isomorphism induced by the equality is the equality on the right components transported through T.

Русский

Если X и Y равны как объекты в StructuredArrow S T, то правая компонента канонического изоморфизма, индуцированного равенством, равна равенству правых компонент, перенесённому сквозь T.

LaTeX

$$$((\mathrm{eqToHom}\, h).right) = \mathrm{eqToHom}\big( T.map\big( \mathrm{congrArg}\ \mathrm{StructuredArrow.right}\, h \big) \big)$$$

Lean4

@[simp]
theorem eqToHom_right {X Y : StructuredArrow S T} (h : X = Y) : (eqToHom h).right = eqToHom (by rw [h]) :=
  by
  subst h
  simp only [eqToHom_refl, id_right]

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