coyoneda_full

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coyoneda.coyoneda_full

English

The Coyoneda functor is full (duplicate statement to reflect independent entry).

Русский

Функтор Coyoneda полнообразен (повторение утверждения).

LaTeX

$$ Coyoneda Full $$

Lean4

instance coyoneda_full : (coyoneda : Cᵒᵖ ⥤ C ⥤ Type v₁).Full :=
  fullyFaithful.full

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

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

Разделы

Аффилиация

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