instFullFintypeCatLightProfiniteToLightProfinite

English

The functor FintypeCat.toLightProfinite is full, i.e., every morphism between images of objects is induced by a morphism in FintypeCat.

Русский

Функтор FintypeCat.toLightProfinite полный: каждый морфизм между образами объектов проистекает из морфизма в FintypeCat.

LaTeX

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

Lean4

instance : FintypeCat.toLightProfinite.Full :=
  FintypeCat.toLightProfiniteFullyFaithful.full

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