full

Mathlib.CategoryTheory.InducedCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InducedCategory.full

English

The induced functor from the induced category is full.

Русский

Индуцированный функтор из индуцированной категории является полным.

LaTeX

$$$\\operatorname{Full}(\\operatorname{inducedFunctor}(F))$$$

Lean4

instance full : (inducedFunctor F).Full :=
  (fullyFaithfulInducedFunctor F).full

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru