instFaithfulFintypeCatLightProfiniteToLightProfinite

English

The functor from FintypeCat to LightProfinite is faithful, i.e., it injects morphisms (distinct arrows remain distinct).

Русский

Функтор от FintypeCat к LightProfinite верен: различные морфизмы остаются различными после применения функтору.

LaTeX

$$$\text{FintypeCat.toLightProfinite is faithful}$$$

Lean4

instance : FintypeCat.toLightProfinite.Faithful :=
  FintypeCat.toLightProfiniteFullyFaithful.faithful

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