eqToHom_trans — Mathlib

English

Composition of equalities corresponds to composition of morphisms in a coherent way: eqToHom p ≫ eqToHom q = eqToHom (p.trans q).

Русский

Соответствие превращается в композицию гомоморфизмов: eqToHom p ≫ eqToHom q = eqToHom (p.trans q).

LaTeX

$$$ \forall p:q:X=Y, q':Y=Z,\; eqToHom(p) \;\gg\; eqToHom(q) = eqToHom(p \cdot q). $$$

Lean4

@[reassoc (attr := simp)]
theorem eqToHom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) : eqToHom p ≫ eqToHom q = eqToHom (p.trans q) :=
  by
  cases p
  cases q
  simp

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