mkFunctor_map_inclLeft — Mathlib

English

For any morphism f: c ⟶ c' in C, the map of mkFunctor along inclLeft sends f to F.map f.

Русский

Для любого морфизма f: c ⟶ c' в C отображение mkFunctor вдоль inclLeft отправляет f в F.map f.

LaTeX

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

Lean4

@[simp]
theorem mkFunctor_map_inclLeft {c c' : C} (f : c ⟶ c') : (mkFunctor F G α).map ((inclLeft C D).map f) = F.map f :=
  rfl

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