instFullContActionFintypeCatAutFunctorFunctorToContAction

English

The functor functorToContAction is full; every morphism between Aut F-sets in ContAction arises from a morphism in C.

Русский

Функтор (functorToContAction) полно: любая морфизм между Aut F-множестами в ContAction получается как образ морфизма в C.

LaTeX

$$$\\big(\\mathrm{functorToContAction}\\;F\\big)\\;\\text{is full}$$$

Lean4

instance : (functorToContAction F).Full :=
  inferInstanceAs <| (ObjectProperty.lift _ _ _).Full

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