instFaithfulSingle — Mathlib

English

For every j, the functor single V c j is faithful.

Русский

Для каждого j функтор single V c j сохраняет различимость и он является верным (faithful).

LaTeX

$$$$ \text{For all } j,\; (\text{single } V\ c\ j).\text{Faithful} $$$$

Lean4

instance (j : ι) : (single V c j).Faithful where
  map_injective {A B f g}
    w := by
    rw [← cancel_mono (singleObjXSelf c j B).inv, ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self, ←
      single_map_f_self, w]

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