congr_map — Mathlib

English

An equality of Prefunctors yields an equality of their action on any morphism.

Русский

Равенство префункторов порождает равенство их отображений на любой морфизм.

LaTeX

$$$e\\!:\\ F=G \\Rightarrow Q\\uarr{hom}(F.map f) = G.map f\\;\\text{(with endpoints transported by }e)$$$

Lean4

theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) :
    F.map f = F.map g := by rw [h]

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