eqToHom_map_comp_apply — Mathlib

English

For p: X = Y and q: Y = Z and x ∈ F.obj X, F.map (eqToHom q) (F.map (eqToHom p) x) equals F.map (eqToHom (p.trans q)) x.

Русский

Для p: X=Y и q: Y=Z и x ∈ F(X) выполняется F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom (p.trans q)) x.

LaTeX

$$$$ F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom (p.trans q)) x. $$$$

Lean4

@[simp]
theorem eqToHom_map_comp_apply (p : X = Y) (q : Y = Z) (x : F.obj X) :
    F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom <| p.trans q) x := by cat_disch

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