map_comp_heq — Mathlib

English

If hx, hy, hz express equality of objects X, Y, Z across F and G, and hf, hg express HEq of F.map f and G.map f, then F.map (f ≫ g) ≍ G.map (f ≫ g).

Русский

Если hx, hy, hz выражают равенство объектов X, Y, Z между F и G, а hf, hg выражают HEq F.map f и G.map f, то F.map (f ≫ g) ≍ G.map (f ≫ g).

LaTeX

$$$ F.map(f \\;\\circ\\; g) \\mathrel{≍} G.map(f \\;\\circ\\; g) $$$

Lean4

theorem map_comp_heq (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z) (hf : F.map f ≍ G.map f)
    (hg : F.map g ≍ G.map g) : F.map (f ≫ g) ≍ G.map (f ≫ g) :=
  by
  rw [F.map_comp, G.map_comp]
  congr

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