postcomp_map_heq — Mathlib

English

If H: D ⥤ E and hx, hy witness equality of F and G on X and Y, and hmap: F.map f ≍ G.map f, then (F ⋙ H).map f ≍ (G ⋙ H).map f.

Русский

Если H: D ⥤ E и hx, hy равенства F и G на X и Y и hmap: F.map f ≍ G.map f, тогда (F ⋙ H).map f ≍ (G ⋙ H).map f.

LaTeX

$$$ (F \\cdot H).map f \\mathrel{\\equiv} (G \\cdot H).map f $$$

Lean4

theorem postcomp_map_heq (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : F.map f ≍ G.map f) :
    (F ⋙ H).map f ≍ (G ⋙ H).map f := by
  dsimp
  congr

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