eqToHom_left — Mathlib

English

Given an equality h : X = Y in CostructuredArrow, the left component of eqToHom h equals the left component after rewriting by h.

Русский

При равенстве h : X = Y в CostructuredArrow левая часть (eqToHom h).left равна левой части после преобразования по h.

LaTeX

$$$(\\mathrm{eqToHom}\, h).\\text{left} = \\mathrm{eqToHom}\\,(by\\, rw\\, h)$$$

Lean4

@[simp]
theorem eqToHom_left {X Y : CostructuredArrow S T} (h : X = Y) : (eqToHom h).left = eqToHom (by rw [h]) :=
  by
  subst h
  simp only [eqToHom_refl, id_left]

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