precomp_map_heq — Mathlib

English

If H: E ⥤ C and F ≍ G as functors C ⥤ D with hmap property, then precomposing with H preserves HEq: (H ⋙ F) ≍ (H ⋙ G).

Русский

Если H: E ⥤ C и F ≍ G как функторы C ⥤ D, то предварительная композиция с H сохраняет HEq: (H ⋙ F) ≍ (H ⋙ G).

LaTeX

$$$ (H \\;\\cdot\\; F) \\mathrel{≍} (H \\;\\cdot\\; G) $$$

Lean4

theorem precomp_map_heq (H : E ⥤ C) (hmap : ∀ {X Y} (f : X ⟶ Y), F.map f ≍ G.map f) {X Y : E} (f : X ⟶ Y) :
    (H ⋙ F).map f ≍ (H ⋙ G).map f :=
  hmap _

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