mkFunctor_map_inclRight — Mathlib

English

For any morphism f: d ⟶ d' in D, the mkFunctor map along inclRight sends f to G.map f.

Русский

Для любого морфизма f: d ⟶ d' в D отображение mkFunctor вдоль inclRight отправляет f в G.map f.

LaTeX

$$$ (\mathrm{mkFunctor} F G \alpha).\mathrm{map}( (\mathrm{inclRight} C D).\mathrm{map} f) = G.\mathrm{map} f $$$

Lean4

@[simp]
theorem mkFunctor_map_inclRight {d d' : D} (f : d ⟶ d') : (mkFunctor F G α).map ((inclRight C D).map f) = G.map f :=
  rfl

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