faithful_whiskeringRight_obj — Mathlib

English

If F is faithful, then the whiskeringRight by F is faithful at the level of objects.

Русский

Если F верен, то whiskeringRight по F является верным на уровне объектов.

LaTeX

$$$ \\text{faithful\\_whiskeringRight\\_obj}$$$

Lean4

instance faithful_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] : ((whiskeringRight C D E).obj F).Faithful where
  map_injective
    hαβ := by
    ext X
    exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

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